1,721,163 research outputs found
Modelling Concurrent Computations: from Contextual Petri Nets to Graph Grammars
No full textGraph grammars (or graph transformation systems), originally introduced as a generalization of string grammars, can be seen as a powerful formalism for the specification of concurrent and distributed systems, which properly extends Petri nets. The idea is that the state of a distributed system can be naturally represented (at a suitable level of abstraction) as a graph and local state transformations can be expressed as production applications.
With the aim of consolidating the foundations of the concurrency theory for graph transformation systems, the thesis extends to this more general setting some fundamental approaches to the semantics coming from Petri net theory. More specifically, focusing on the so-called double pushout (DPO) algebraic approach to graph rewriting, the thesis provides graph transformation systems with truly concurrent semantics based on (concatenable) processes and on a Winskel's style unfolding construction, as well as with more abstract semantics based on event structures and domains.
The first part of the thesis studies two generalizations of Petri nets, already known in the literature, which reveal a close relationship with graph transformation systems, namely contextual nets (also called nets with read, activator or test arcs) and inhibitor nets (or nets with inhibitor arcs). Extending Winskel's seminal work on safe nets, the truly concurrent semantics of contextual nets is given via a chain of coreflections leading from the category of contextual nets to the category of finitary coherent prime algebraic domains. A basic role is played by asymmetric event structures, which generalize prime event structures by allowing a non-symmetric conflict relation. The work is then generalized to inhibitor nets, where, due to the non-monotonicity of the enabling, the causal structure of computations is far more complex, and a new, very general, notion of event structure, called inhibitor event structure, is needed to faithfully describe them.
The second part of the thesis, relying on the conceptual basis drawn in the first part, focuses on graph grammars. Inhibitor event structures turn out to be expressive enough to model graph grammar computations, and the theory developed for contextual and inhibitor nets, comprising the unfolding and the (concatenable) process semantics, can be lifted to graph grammars. The developed semantics is shown to to be consistent also with the classical theory of concurrency for DPO graph grammars relying on shift-equivalence
A causal view on non-interference
No full textThe concept of non-interference has been introduced to characterise the absence of undesired information flows in a computing system. Although it is often explained referring to an informal notion of causality - the activity involving the part of the system with higher level of confidentiality should not cause any observable effect at lower levels - it is almost invariably formalised in terms of interleaving semantics. Here we focus on Petri nets and on the BNDC (Bisimilarity-based Non-Deducibility on Composition) property, a formalisation of non-interference widely studied in the literature. We show that BNDC admits natural characterisations based on the unfolding semantics - a classical true concurrent semantics for Petri nets - in terms of causalities and conflicts between high and low level activities. This leads to algorithms for checking BNDC on various classes of Petri nets, based on the construction of suitable complete prefixes of the unfolding. We also developed a prototype tool UBIC (Unfolding-Based Interference Checker), working on safe Petri nets, which provides promising results in terms of efficiency
Model Checking a Logic for True Concurrency
Full text linkWe study the model-checking problem for a logic for true concurrency, whose formulae predicate about events in computations and their causal dependencies. The logic, which represents the logical counterpart of history-preserving bisimilarity, is naturally interpreted over event structures or any formalism that can be given a causal semantics, like Petri nets. It includes least and greatest fixpoint operators and thus it can express properties of infinite computations. Since the event structure associated with a system is typically infinite (even if the system is finite state), already the decidability of model-checking is non-trivial. We first develop a local model-checking technique based on a tableau system, for which, over a class of event structures satisfying a suitable regularity condition, referred to as strong regularity, we prove termination, soundness, and completeness. The tableau system allows for a clean and intuitive proof of decidability, but a direct implementation of the procedure can be extremely inefficient. For easing the development of a more efficient model-checking technique, we move to an automata-theoretic framework. Given a formula and a strongly regular event structure, we show how to construct a parity tree automaton whose language is non-empty if and only if the event structure satisfies the formula. The automaton is usually infinite. We discuss how it can be quotiented to an equivalent finite automaton, where emptiness can be checked effectively. To show the applicability of the approach, we discuss how it instantiates to finite safe Petri nets, providing also a corresponding proof-of-concept model-checking tool
Concurrency for graph grammars (in a Petri net shell)
No full textM. Bauderon and A. Corradini, eds., Elsevier
Many-to-many information flow policies
No full textInformation flow techniques typically classify information according to suitable security levels and enforce policies that are based on binary relations between individual levels, e.g., stating that information is allowed to flow from one level to another. We argue that some information flow properties of interest naturally require coordination patterns that involve sets of security levels rather than individual levels: some secret information could be safely disclosed to a set of confidential channels of incomparable security levels, with individual leaks considered instead illegal; a group of competing agencies might agree to disclose their secrets, with individual disclosures being undesired, etc. Motivated by this, we study a semantic foundation for such properties based on causal models of computation. We propose a simple language for expressing information flow policies where the usual admitted flow relation between individual security levels is replaced by a relation between sets of security levels, thus allowing to capture coordinated flows of information. The flow of information is expressed in terms of causal dependencies and the satisfaction of a policy is defined with respect to an event structure that is assumed to capture the causal structure of system computations. We also preliminarily explore possibilities for practical applicability of our approach by focusing on systems specified as safe Petri nets, a formalism with a well-established causal semantics. We show how unfolding-based verification techniques for Petri nets can be adopted for solving the problem of checking policy satisfaction
Non-interference by Unfolding
No full textThe concept of non-interference has been introduced to characterise the absence of undesired information flows in a computing system. Although it is often explained referring to an informal notion of causality - the activity involving the part of the system with higher level of confidentiality should not cause any observable effect at lower levels - it is almost invariably formalised in terms of interleaving semantics. Here we focus on Petri nets and on the BNDC property (Bisimilarity-based Non-Deducibility on Composition), a formalisation of non-interference widely studied in the literature. We show that BNDC admits natural characterisations based on the unfolding semantics - a classical true concurrent semantics for Petri nets - in terms of causalities and conflicts between high and low level activities. This leads to an algorithm for checking BNDC for safe Petri nets which relies on the construction of suitable complete prefixes of the unfolding. A prototype tool provides very promising results
Automata for true concurrency properties
Full text linkWe present an automata-theoretic framework for the model checking of true concurrency properties. These are specified in a fixpoint logic, corresponding to history-preserving bisimilarity, capable of describing events in computations and their dependencies. The models of the logic are event structures or any formalism which can be given a causal semantics, like Petri nets. Given a formula and an event structure satisfying suitable regularity conditions we show how to construct a parity tree automaton whose language is non-empty if and only if the event structure satisfies the formula. The automaton, due to the nature of event structure models, is usually infinite. We discuss how it can be quotiented to an equivalent finite automaton, where emptiness can be checked effectively. In order to show the applicability of the approach, we discuss how it instantiates to finite safe Petri nets. As a proof of concept we provide a model checking tool implementing the technique
- …
