A new algorithm is introduced for analyzing possible nesting in Mobile Ambient calculus. It improves both time and space complexities of the technique proposed by Nielson and Seidl. The improvements are achieved by enhancing the data structure …
We present an algorithm that computes in a linear number of symbolic steps (O(|V|)) the strongly connected components (sccs) of a graph G = represented by an Ordered Binary Decision Diagram (OBDD). This result matches the complexity of the …
The analysis of large amounts of data, produced as (numerical) traces of in vivo, in vitro and in silico experiments, has become a central activity for many biologists and biochemists. Recent advances in the mathematical modeling and computation of …
We discuss the formalization of Abadi and Cardelli's imps, a paradigmatic object-based calculus with types and side effects, in Co-Inductive Type Theories, such as the Calculus of (Co)Inductive Constructions (CC(Co)Ind). Instead of representing …
Information flow security in a multilevel system aims at guaranteeing that no high level information is revealed to low level users, even in the presence of any possible malicious process. Persistent_BNDC (P_BNDC, for short) is an information-flow …
In this paper we propose a semantically well-founded combination of the constraint solvers used in the constraint programming languages CLP (SET) and CLP(ℱD). This work demonstrates that it is possible to provide efficient executions (through CLP …
We propose a parametric introduction of intensionally defined sets into any CLP(D) language. The result is a language CLP(D), where constraints over sets of elements of D and over sets of sets of elements, and so on, can be expressed. The semantics …
Most of the observable natural phenomena exhibit a mixed discrete-continuous behavior characterized by laws changing according to a phase cycle. Such behaviors can be modeled in a very natural way by a class of automata called hybrid automata. In …
The systematic development of complex systems usually relies on a stepwise refinement procedure from an abstract specification to a more concrete one that can finally be implemented. The use of refinement operators preserving system properties is …