Catálogo de publicaciones - libros

Soundness of compositional reasoning rules depends on computational models and sometimes is rather involved. Verifiers are therefore forced to mould their problems into a handful of sound compositional rules known to them. In this paper, a syntactic approach to establishing soundness of compositional rules in automated compositional reasoning is presented. Not only can our work justify all compositional rules known to us, but also derive new circular rules by intuitionistic reasoning automatically. Invertibility issues are also briefly discussed in the paper.

We propose the first compositional event structure semantics for a very expressive -calculus, generalising Winskel’s event structures for CCS. The -calculus we model is the I-calculus with recursive definitions and summations. First we model the calculus, introducing a notion of dynamic renaming to the standard operators on event structures. Then we model the calculus, for which a new additional operator, called , is necessary for representing causality due to new name binding. The semantics are shown to be operationally adequate and sound with respect to bisimulation.

We propose and study a translation of a pi-calculus without sums nor replication/recursion into an untyped and essentially promotion-free version of differential interaction nets. We define a transition system of labeled processes and a transition system of labeled differential interaction nets. We prove that our translation from processes to nets is a bisimulation between these two transition systems. This shows that differential interaction nets are sufficiently expressive for representing concurrency and mobility, as formalized by the pi-calculus.

D is a simple distributed extension of the -calculus in which agents are explicitly located, and may use an explicit migration construct to move between locations.

We introduce passports to control those migrations; in order to gain access to a location agents are now expected to show some credentials, granted by the destination location. Passports are tied to specific locations, from which migration is permitted. We describe a type system for these passports, which includes a novel use of dependent types, and prove that well-typing enforces the desired behaviour in migrating processes.

Passports allow locations to control incoming processes. This induces major modifications to the observations which can be made of agent-based systems. Using the type system we describe these observations, and use them to build a notion of observational equivalence. Finally we provide a complete proof technique in the form of a bisimilarity for establishing equivalences between systems.

Reactive Systems Leifer and Milner allow to derive from a reaction semantics definition an LTS equipped with a bisimilarity relation which is a congruence. This theory has been extended by the authors (together with Barbara König) in order to handle saturated bisimilarity, a coarser equivalence that is more adequate for some interesting formalisms, such as logic programming and open pi-calculus. In this paper we recast the theory of Reactive Systems inside Universal Coalgebra. This construction is particularly useful for saturated bisimilarity, which can be seen as final semantics of Normalized Coalgebras. These are structured coalgebras (not bialgebras) where the sets of transitions are minimized rather than maximized as in saturated LTS, still yielding the same semantics. We give evidence the effectiveness of our approach minimizing an Open Petri net in a category of Normalized Coalgebras.

We study the construction of labelled transition systems from reactive systems defined over , a computational meta-model which subsumes other variants of bigraphs. First we consider wide transition systems whose labels are all those generated by the IPO construction; the corresponding bisimulation is always a congruence. Then, we show that these LTSs can be simplified further by restricting to a subclass of labels, which can be characterized syntactically.

We apply this theory to the Fusion calculus: we give an encoding of Fusion in directed bigraphs, and describe its simplified wide transition system and corresponding bisimulation.

The notion of innocent strategy was introduced by Hyland and Ong in order to capture the interactive behaviour of -terms and PCF programs. An innocent strategy is defined as an alternating strategy with partial memory, in which the strategy plays according to its view. Extending the definition to non-alternating strategies is problematic, because the traditional definition of views is based on the hypothesis that Opponent and Proponent alternate during the interaction. Here, we take advantage of the diagrammatic reformulation of alternating innocence in asynchronous games, in order to provide a tentative definition of innocence in non-alternating games. The task is interesting, and far from easy. It requires the combination of true concurrency and game semantics in a clean and organic way, clarifying the relationship between asynchronous games and concurrent games in the sense of Abramsky and Melliès. It also requires an interactive reformulation of the usual acyclicity criterion of linear logic, as well as a directed variant, as a scheduling criterion.

This paper introduces strong bisimulation for continuous-time Markov decision processes (CTMDPs), a stochastic model which allows for a nondeterministic choice between exponential distributions, and shows that bisimulation preserves the validity of CSL . To that end, we interpret the semantics of CSL —a stochastic variant of CSL for continuous-time Markov chains—on CTMDPs and show its measure-theoretic soundness. The main challenge faced in this paper is the proof of logical preservation that is substantially based on measure theory.

We consider a class of finite -player games (Markov decision processes) where the winning objectives are specified in the branching-time temporal logic qPECTL* (an extension of the qualitative PCTL*). We study decidability and complexity of existence of a winning strategy in these games. We identify a fragment of qPECTL* called detPECTL* for which the existence of a winning strategy is decidable in exponential time, and also the winning strategy can be computed in exponential time (if it exists). Consequently we show that every formula of qPECTL can be translated to a formula of detPECTL* (in exponential time) so that the resulting formula is equivalent to the original one over finite Markov chains. From this we obtain that for the whole qPECTL*, the existence of a winning finite-memory strategy is decidable in double exponential time. An immediate consequence is that the existence of a winning finite-memory strategy is decidable for the qualitative fragment of PCTL* in triple exponential time. We also obtain a single exponential upper bound on the same problem for the qualitative PCTL. Finally, we study the power of finite-memory strategies with respect to objectives described in the qualitative PCTL.

We propose a new model for timed games, based on concurrent game structures (CGSs). Compared to the classical of Asarin [8], our timed CGSs are “more concurrent”, in the sense that they always allow all the agents to act on the system, independently of the delay they want to elapse before their action. Timed CGSs weaken the “element of surprise” of timed game automata reported by de Alfaro [15].

We prove that our model has nice properties, in particular that model-checking timed CGSs against timed ATL is decidable region abstraction, and in particular that strategies are “region-stable” if winning objectives are. We also propose a new extension of TATL, containing ATL*, which we call TALTL. We prove that model-checking this logic remains decidable on timed CGSs. Last, we explain how our algorithms can be adapted in order to rule out Zeno (co-)strategies, based on the ideas of Henzinger [15,20].