Catálogo de publicaciones - libros

We give logical characterizations of bisimulation relations for the probabilistic automata of Segala in terms of three Hennessy-Milner style logics. The three logics characterize strong, strong probabilistic and weak probabilistic bisimulation, and differ only in the kind of diamond operator used. Compared to the Larsen and Skou logic for reactive systems, these logics introduce a new operator that measures the probability of the set of states that satisfy a formula. Moreover, the satisfaction relation is defined on measures rather than single states. We rederive previous results of Desharnais et al. by defining sublogics for Reactive and Alternating Models viewed as restrictions of probabilistic automata. Finally, we identify restrictions on probabilistic automata, weaker than those imposed by the Alternating Models, that preserve the logical characterization of Desharnais et al. These restrictions require that each state either enables several ordinary transitions or enables a single probabilistic transition.

We use the framework of biorthogonality to introduce a novel semantic definition of the concept of barb (basic observable) for process calculi. We develop a uniform basic theory of barbs and demonstrate its robustness by showing that it gives rise to the correct observables in specific process calculi which model synchronous, asynchronous and broadcast communication regimes.

We investigate some aspects of proof methods for the termination of (extensions of) the second-order λ -calculus in presence of union and existential types. We prove that Girard’s reducibility candidates are stable by union iff they are exactly the non-empty sets of terminating terms which are downward-closed w.r.t. a weak observational preorder. We show that this is the case for the Curry-style second-order λ -calculus. As a corollary, we obtain that reducibility candidates are exactly the Tait’s saturated sets that are stable by reduction. We then extend the proof to a system with product, co-product and positive iso-recursive types.

By adding the complement operator (¬), extended regular expressions ( ERE ) can encode regular languages non-elementarily more succinctly than regular expressions. The ERE membership problem asks whether a word w of size n belongs to the language of an ERE R of size m . Unfortunately, the best known membership algorithms are either non-elementary in m or otherwise require space Ω ( n ^2) and time Ω ( n ^3); since in many practical applications n can be very large, these space and time requirements could be prohibitive. In this paper we present an ERE membership algorithm that runs in space O ( n ·(log n  +  m ) ·2^ m ) and time O ( n ^2 ·(log n  +  m ) ·2^ m ). The presented algorithm outperforms the best known algorithms when n is exponentially larger than m .

Some decision problems related to balanced context-free languages are important for their application to the static analysis of programs generating XML strings. One such problem is the balancedness problem which decides whether or not the language of a given context-free grammar (CFG) over a paired alphabet is balanced. Another important problem is the validation problem which decides whether or not the language of a CFG is contained by that of a regular hedge grammar (RHG). This paper gives two new results; (1) the balancedness problem is in PTIME; and (2) the CFG-RHG containment problem is 2EXPTIME-complete.

We introduce an extension of Hoare logic for call-by-value higher-order functions with ML-like local reference generation. Local references may be generated dynamically and exported outside their scope, may store higher-order functions and may be used to construct complex mutable data structures. This primitive is captured logically using a predicate asserting reachability of a reference name from a possibly higher-order datum and quantifiers over hidden references. The logic enjoys three completeness properties: relative completeness, a logical characterisation of the contextual congruence and derivability of characteristic formulae. The axioms for reachability and local invariants play a fundamental role in reasoning about non-trivial programs combining higher-order procedures and dynamically generated references.