Catálogo de publicaciones - libros

We study the concept of choice for true concurrency models such as prime event structures and safe Petri nets. We propose a dynamic variation of the notion of cluster previously introduced for nets. This new object is defined for event structures, it is called a branching cell . Our aim is to bring an interpretation of branching cells as a right notion of “local state”, for concurrent systems. We illustrate the above claim through applications to probabilistic concurrent models. In this respect, our results extends in part previous work by Varacca-Völzer-Winskel on probabilistic confusion free event structures. We propose a construction for probabilities over so-called locally finite event structures that makes concurrent processes probabilistically independent—simply attach a dice to each branching cell; dices attached to concurrent branching cells are thrown independently. Furthermore, we provide a true concurrency generalization of Markov chains, called Markov nets. Unlike in existing variants of stochastic Petri nets, our approach randomizes Mazurkiewicz traces, not firing sequences. We show in this context the Law of Large Numbers (LLN), which confirms that branching cells deserve the status of local state. Our study was motivated by the stochastic modeling of fault propagation and alarm correlation in telecommunications networks and services. It provides the foundations for probabilistic diagnosis, as well as the statistical distributed learning of such models.

Fault diagnosis consists in observing behaviours of systems, and in detecting online whether an error has occurred or not. In the context of discrete event systems this problem has been well-studied, but much less work has been done in the timed framework. In this paper, we consider the problem of diagnosing faults in behaviours of timed plants. We focus on the problem of synthesizing fault diagnosers which are realizable as deterministic timed automata, with the motivation that such diagnosers would function as efficient online fault detectors. We study two classes of such mechanisms, the class of deterministic timed automata (DTA) and the class of event-recording timed automata (ERA). We show that the problem of synthesizing diagnosers in each of these classes is decidable, provided we are given a bound on the resources available to the diagnoser. We prove that under this assumption diagnosability is 2EXPTIME-complete in the case of DTA’s whereas it becomes PSPACE-complete for ERA’s.

Nominal calculi have been shown very effective to formally model a variety of computational phenomena. The models of nominal calculi have often infinite states, thus making model checking a difficult task. In this note we survey some of the approaches for model checking nominal calculi. Then, we focus on History-Dependent automata , a syntax-free automaton-based model of mobility. History-Dependent automata have provided the formal basis to design and implement some existing verification toolkits. We then introduce a novel syntax-free setting to model the symbolic semantics of a nominal calculus. Our approach relies on the notions of reactive systems and observed borrowed contexts introduced by Leifer and Milner, and further developed by Sassone, Lack and Sobocinski. We argue that the symbolic semantics model based on borrowed contexts can be conveniently applied to web service discovery and binding.

The general aim of this talk is to advocate a combinatorial perspective, together with its methods, in the investigation and study of models of computation structures. This, of course, should be taken in conjunction with the well-established views and methods stemming from algebra, category theory, domain theory, logic, type theory,  etc . In support of this proposal I will show how such an approach leads to interesting connections between various areas of computer science and mathematics; concentrating on one such example in some detail. Specifically, I will consider the line of my research involving denotational models of the pi calculus and algebraic theories with variable-binding operators, indicating how the abstract mathematical structure underlying these models fits with that of Joyal’s combinatorial species of structures. This analysis suggests both the unification and generalisation of models, and in the latter vein I will introduce generalised species of structures and their calculus. These generalised species encompass and generalise various of the notions of species used in combinatorics. Furthermore, they have a rich mathematical structure (akin to models of Girard’s linear logic) that can be described purely within Lawvere’s generalised logic. Indeed, I will present and treat the cartesian closed structure, the linear structure, the differential structure,  etc. of generalised species axiomatically in this mathematical framework. As an upshot, I will observe that the setting allows for interpretations of computational calculi (like the lambda calculus, both typed and untyped; the recently introduced differential lambda calculus of Ehrhard and Regnier;  etc ) that can be directly seen as translations into a more basic elementary calculus of interacting agents that compute by communicating and operating upon structured data.

Structural congruences have been used to define the semantics and to capture inherent properties of language constructs. They have been used as an addendum to transition system specifications in Plotkin’s style of Structural Operational Semantics (SOS). However, there has been little theoretical work on establishing a formal link between these two semantic specification frameworks. In this paper, we give an interpretation of structural congruences inside the transition system specification framework. This way, we extend a number of well-behavedness meta-theorems for SOS (such as well-definedness of the semantics and congruence of bisimilarity) to the extended setting with structural congruences.

We propose an SOS transition rule format for the generative model of probabilistic processes. Transition rules are partitioned in several strata, giving rise to an ordering relation analogous to those introduced by Ulidowski and Phillips for classic process algebras. Our rule format guarantees that probabilistic bisimulation is a congruence w.r.t. process algebra operations. Moreover, our rule format guarantees that process algebra operations preserve semistochasticity of processes, i.e. the property that the sum of the probability of the moves of any process is either 0 or 1. Finally, we show that most of operations of the probabilistic process algebras studied in the literature are captured by our format, which, therefore, has practical applications.

Two process–algebraic approaches have been developed for comparing two bisimulation–equivalent processes with respect to speed: the one of Moller/Tofts equips actions with lower time bounds, while the one by Lüttgen/Vogler considers upper time bounds instead. This paper sheds new light on both approaches by testifying to their close relationship. We introduce a general, intuitive concept of “faster–than”, which is formalised by a notion of amortised faster–than preorder . When closing this preorder under all contexts, exactly the two faster–than preorders investigated by Moller/Tofts and Lüttgen/Vogler arise. For processes incorporating both lower and upper time bounds we also show that the largest precongruence contained in the amortised faster–than preorder is not a proper preorder but a timed bisimulation. In the light of this result we systematically investigate under which circumstances the amortised faster–than preorder degrades to an equivalence.

We study the concept of choice for true concurrency models such as prime event structures and safe Petri nets. We propose a dynamic variation of the notion of cluster previously introduced for nets. This new object is defined for event structures, it is called a branching cell . Our aim is to bring an interpretation of branching cells as a right notion of “local state”, for concurrent systems. We illustrate the above claim through applications to probabilistic concurrent models. In this respect, our results extends in part previous work by Varacca-Völzer-Winskel on probabilistic confusion free event structures. We propose a construction for probabilities over so-called locally finite event structures that makes concurrent processes probabilistically independent—simply attach a dice to each branching cell; dices attached to concurrent branching cells are thrown independently. Furthermore, we provide a true concurrency generalization of Markov chains, called Markov nets. Unlike in existing variants of stochastic Petri nets, our approach randomizes Mazurkiewicz traces, not firing sequences. We show in this context the Law of Large Numbers (LLN), which confirms that branching cells deserve the status of local state. Our study was motivated by the stochastic modeling of fault propagation and alarm correlation in telecommunications networks and services. It provides the foundations for probabilistic diagnosis, as well as the statistical distributed learning of such models.

We study a process calculus which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch’s probabilistic automata. We consider various strong and weak behavioral equivalences, and we provide complete axiomatizations for finite-state processes, restricted to guarded definitions in case of the weak equivalences. We conjecture that in the general case of unguarded recursion the “natural” weak equivalences are undecidable. This is the first work, to our knowledge, that provides a complete axiomatization for weak equivalences in the presence of recursion and both nondeterministic and probabilistic choice.

We study the interaction between non-deterministic and probabilistic behaviour in systems with continuous state spaces, arbitrary probability distributions and uncountable branching. Models of such systems have been proposed previously. Here, we introduce a model that extends probabilistic automata to the continuous setting. We identify the class of schedulers that ensures measurability properties on executions, and show that such measurability properties are preserved by parallel composition. Finally, we demonstrate how these results allow us to define an alternative notion of weak bisimulation in our model.