Articles

DAZL: Density-aware zone-based packet forwarding in vehicular networks

Meireles R., Steenkiste P., Barros J.

IEEE Vehicular Networking Conference, VNC

2012

Abstract:

Multi-hop message forwarding based on geographic coordinates is a fundamental building block for vehicular communication. However, the unstable links and wide range of node densities make it challenging to design an algorithm suitable for vehicular use. We introduce DAZL, a new forwarding protocol that combines three concepts in a novel way. First, multiple nodes cooperate in packet forwarding. Compared with traditional single relay schemes, this provides robustness against changes in topology and packet delivery rates. Second, network-layer slotting is used to control duplication and contention in high density scenarios. Third, a distributed prioritization algorithm is used to opportunistically maximize hop length. Through both experiments and simulations, we show that DAZL provides improvements of up to 60% in throughput over single relay forwarding, while ensuring low latency and replication.

Decidability and complexity for ω-regular properties of stochastic systems

Henriques D., Biscaia M., Baltazar P., Mateus P.

Logic Journal of the IGPL

2012

Abstract:

Herein we study the probabilization of Quantified Linear Temporal Logic, which we call PQLTL. PQLTL can reason about any semialgebraic constrain over probabilities of paths of a Markov chain satisfying a QLTL formulae. PQLTL is related with other commonly used probabilistic temporal logics (such as PLTL, PCTL and PCTL*) that were devised only to specify properties for which model checking algorithms are amenable and whose basic results, such as completeness and decidability, were never investigated. In this article, we devise a strong and a weak SAT algorithm for PQLTL. The former relies in [n+2]-EXPSPACE and the latter in [n+1]-EXPSPACE where n is the alternation depth of the quantifiers in the input formula. The weak SAT algorithm for the existential fragment, which has all the expressive power of PQLTL, is in EXPSPACE. Another relevant fragment of PQLTL is the linear closure of PCTL* without nesting of the probability operator. We show that the SAT problem for this fragment is PSPACE complete. Capitalizing in these results, we derive a complete calculus for PQLTL and illustrate it with a toy example.

Decidability of approximate skolem problem and applications to logical verification of dynamical properties of markov chains

Biscaia M., Henriques D., Mateus P.

ACM Transactions on Computational Logic

2014

Abstract:

When studying probabilistic dynamical systems, temporal logic has typically been used to analyze path properties. Recently, there has been some interest in analyzing the dynamical evolution of state probabilities of these systems. In this article, we show that verifying linear temporal properties concerning the state evolution induced by a Markov chain is equivalent to the decidability of the Skolem problem — a long-standing open problem in Number Theory. However, from a practical point of view, usually it is enough to check properties up to some acceptable error bound ε. We show that an approximate version of the Skolem problem is decidable, and that it can be applied to verify, up to arbitrarily small ε, linear temporal properties of the state evolution induced by a Markov chain.

Decision Support Dashboard for Traffic and Environment Analysis of a Smart City

Pereira J., Sargento S., Fernandes J.M.

Proceedings of the 4th International Conference on Vehicle Technology and Intelligent Transport Systems (VEHITS 2018)

2018

Abstract:

Porto city has an in-place infrastructure of fixed and moving sensors in more than 400 buses and roadside units, with both GPS and mobility sensors in moving elements, and with environmental sensors in fixed units. This infrastructure can provide valuable data that can extract information to better understand the city and, eventually, support actions to improve the city mobility, urban planning, and environment. Our system provides a full stack integration of the information into a city dashboard that displays and correlates the data generated from buses and fixed sensors, allowing different visualizations over the traffic and environment in the city, and decisions over the current status of the city. A good example relates bus speed variation with possible anomalies on the road or traffic jams. Visualizing such information and getting alarms on anomalies can be a valuable tool to a city manager when taking urban planning decisions to improve the city mobility

Declarative coordination of graph-based parallel programs

Cruz F., Rocha R., Goldstein S.C.

Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP

2016

Abstract:

Declarative programming has been hailed as a promising approach to parallel programming since it makes it easier to reason about programs while hiding the implementation details of parallelism from the programmer. However, its advantage is also its disadvantage as it leaves the programmer with no straightforward way to optimize programs for performance. In this paper, we introduce Coordinated Linear Meld (CLM), a concurrent forward-chaining linear logic programming language, with a declarative way to coordinate the execution of parallel programs allowing the programmer to specify arbitrary scheduling and data partitioning policies. Our approach allows the programmer to write graph-based declarative programs and then optionally to use coordination to fine-tune parallel performance. In this paper we specify the set of coordination facts, discuss their implementation in a parallel virtual machine, and show—through example—how they can be used to optimize parallel execution. We compare the performance of CLM programs against the original uncoordinated Linear Meld and several other frameworks.

Deep Convolutional Artery/Vein Classification of Retinal Vessels

Meyer M.I., Galdran A., Costa P., Mendonça A.M., Campilho A.

ICIAR 2018: Image Analysis and Recognition

2018

Abstract:

The classification of retinal vessels into arteries and veins in eye fundus images is a relevant task for the automatic assessment of vascular changes. This paper presents a new approach to solve this problem by means of a Fully-Connected Convolutional Neural Network that is specifically adapted for artery/vein classification. For this, a loss function that focuses only on pixels belonging to the retinal vessel tree is built. The relevance of providing the model with different chromatic components of the source images is also analyzed. The performance of the proposed method is evaluated on the RITE dataset of retinal images, achieving promising results, with an accuracy of 96% on large caliber vessels, and an overall accuracy of 84% .

Dependent session types via intuitionistic linear type theory

Toninho B., Caires L., Pfenning F.

PPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming

2011

Abstract:

We develop an interpretation of linear type theory as dependent session types for a term passing extension of the pi-calculus. The type system allows us to express rich constraints on sessions, such as interface contracts and proof-carrying certification, which go beyond existing session type systems, and are here justified on purely logical grounds. We can further refine our interpretation using proof irrelevance to eliminate communication overhead for proofs between trusted parties. Our technical results include type preservation and global progress, which in our setting naturally imply compliance to all properties declared in interface contracts expressed by dependent types.

Deploying roadside units in sparse vehicular networks: What really works and what does not

Reis A.B., Sargento S., Neves F., Tonguz O.K.

IEEE Transactions on Vehicular Technology

2014

Abstract:

Linear Meld is a concurrent forward-chaining linear logic programming language where logical facts can be asserted and retracted in a structured way. The database of facts is partitioned by the nodes of a graph structure which leads to parallelism if nodes are executed simultaneously. Communication arises whenever nodes send facts to other nodes by fact derivation. We present an overview of the virtual machine that we implemented to run Linear Meld on multicores, including code organization, thread management, rule execution and database organization for efficient fact insertion, lookup and deletion. Although our virtual machine is a work-in-progress, our results already show that Linear Meld is not only capable of scaling graph and machine learning programs but it also exhibits some interesting performance results when compared against other programming languages.

Design and implementation of a multithreaded virtual machine for executing linear logic programs

Cruz F., Rocha R., Goldstein S.C.

PPDP 2014 - Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming

2014

Abstract:

Linear Meld is a concurrent forward-chaining linear logic programming language where logical facts can be asserted and retracted in a structured way. In Linear Meld, a program is seen as a database of logical facts and a set of derivation rules. The database of facts is partitioned by the nodes of a graph structure which leads to parallelism when nodes are executed simultaneously. Due to the foundations on linear logic, rules can retract facts in a declarative and structured fashion, leading to more expressive programs. We present the design and implementation of the virtual machine that we implemented to run Linear Meld on multicores, with particular focus on thread management, code organization, fact indexing, rule execution, and database organization for efficient fact insertion, lookup and deletion. Our results show that the virtual machine is capable of scaling programs with up to 16 threads and also exhibits interesting scalar performance results due to our indexing optimizations.