Abstract Reaction systems are rooted in processes inspired by the functioning of the living cell. The key idea behind the resulting formal model is that such processes are determined by the interactions of biochemical reactions. Moreover, such interactions are based on the fundamental mechanisms of facilitation and inhibition. Since their inception, reaction systems have developed into an extensively investigated model of computation with unique characteristics and a wide range of potential applications. The semantical model of reaction systems is based on the concept of system states consisting of sets of entities, and state transformations enacted by sets of reactions. Another important behavioural property is the non-permanency of the entities, and so data persistence has to be consciously implemented. Issues like this need to be taken into account in all simulations of reaction systems by means of other existing models and tools, such as Petri nets. In this paper, we provide four different Petri net encodings of basic reaction systems operating without interacting with external environment. We start from a naive encoding that is based on the behaviour of a reaction system $$\mathscr {R}$$ only, transforming the transition system of $$\mathscr {R}$$ into a Petri net in the form of a marked graph. Such a solution introduces exponentially many places and transitions. In the subsequent encodings, we cope with this exponentiality ending up with a solution that is polynomial in the size of the original reaction system. We then show how this polynomial encoding can be adapted to provide a polynomial encoding for reaction systems operating with contexts provided by context automata. The encoding method proposed in this paper is modular and can provide a basis for compositional construction of reaction systems.

Abstract Reaction systems are a model of computation inspired by the biochemistry exhibited by living cells. This paper introduces the notion of agency as an extension to the reaction systems formalism, leading to distributed reaction systems. Adding agents in the reaction systems setting, allows for the natural modelling and representation of multi-agent and distributed systems. To support the specification of temporal-epistemic properties of distributed reaction systems, we introduce the logic rs ctlk and present experimental results of its associated model checking procedure run on a biological benchmark of within-cell signal transduction networks. The experimental results are encouraging despite the complexity of the rs ctlk model checking problem that is shown to be pspace -complete.

Abstract Reaction systems are a formal model for computational processing in which reactions operate on sets of entities (molecules) providing a framework for dealing with qualitative aspects of biochemical systems. This paper is concerned with reaction systems in which entities can have discrete concentrations, and so reactions operate on multisets rather than sets of entities. The resulting framework allows one to deal with quantitative aspects of reaction systems, and a bespoke linear-time temporal logic allows one to express and verify a wide range of key behavioural system properties. In practical applications, a reaction system with discrete concentrations may only be partially specified, and the possibility of an effective automated calculation of the missing details provides an attractive design approach. With this idea in mind, the current paper discusses parametric reaction systems with parameters representing unknown parts of hypothetical reactions. The main result is a method aimed at replacing the parameters in such a way that the resulting reaction system operating in a specified external environment satisfies a given temporal logic formula.This paper provides an encoding of parametric reaction systems in smt , and outlines a synthesis procedure based on bounded model checking for solving the synthesis problem. It also reports on the initial experimental results demonstrating the feasibility of the novel synthesis method.

Geo-distributed web-applications (GWA) can be deployed across multiple geographically separated datacenters to reduce the latency of access for users. Finding a suitable deployment for a GWA is challenging due to the requirement to consider a number of different parameters, such as host configurations across a federated infrastructure. The ability to evaluate multiple deployment configurations enables an efficient outcome to be determined, balancing resource usage while satisfying user requirements. We proposeGeoDeploy, a framework designed for finding a deployment solution for GWA. We evaluateGeoDeployusing both a formal algorithmic model and a practical cloud-based deployment. We also compare our approach with other existing techniques.

Elementary net systems with localities (enl-systems) is a class of Petri nets introduced to model globally asynchronous locally synchronous systems (gals), where some of the components can be considered as logically or physically close and acting synchronously, while others can be considered as loosely connected or residing at distant locations and communicating asynchronously with the rest of the system. The specification of the behaviour of a gals system comes very often in the form of a transition system. Automated synthesis based on the regions of transition systems is an approach that allows to construct Petri net models from their transition system specifications. In this paper we focus on developing algorithms and tool support for the synthesis of the enl-systems from transition systems, where transitions are labelled by steps (sets) of executed actions. We pay special attention to the subclass of enl-systems with localised conflicts where there is no conflict between events belonging to different localities. The algorithms are implemented within the workcraft framework.

In reversible computations one is interested in the development of mechanisms allowing to undo the effects of executed actions. The past research has been concerned mainly with reversing single actions. In this paper, we consider the problem of reversing the effect of the execution of groups of actions (steps). Using Petri nets as a system model, we introduce concepts related to this new scenario, generalising notions used in the single action case. We then present properties arising when reverse actions are allowed in place/transition nets (pt-nets). We obtain both positive and negative results, showing that allowing steps makes reversibility more problematic than in the interleaving/sequential case. In particular, we demonstrate that there is a crucial difference between reversing steps which are sets and those which are true multisets. Moreover, in contrast to sequential semantics, splitting reverses does not lead to a general method for reversing bounded pt-nets. We then show that a suitable solution can be obtained by combining split reverses with weighted read arcs. Comment: special issue of PN 2019, after editor changes (Fundamenta Informaticae)

Federated cloud systems increase the reliability and reduce the cost of the computational support. The resulting combination of secure private clouds and less secure public clouds, together with the fact that resources need to be located within different clouds, strongly affects the information flow security of the entire system. In this paper, the clouds as well as entities of a federated cloud system are assigned security levels, and a probabilistic flow sensitive security model for a federated cloud system is proposed. Then the notion of opacity—a notion capturing the security of information flow—of a cloud computing systems is introduced, and different variants of quantitative analysis of opacity are presented. As a result, one can track the information flow in a cloud system, and analyze the impact of different resource allocation strategies by quantifying the corresponding opacity characteristics.

Relational structures based on acyclic relations can successfully model fundamental aspects of concurrent systems behaviour. Examples include Elementary Net systems and Mazurkiewicz traces. There are however cases where more general relational structures are needed. In this paper, we present a general model of relational structures which can be used for a broad class of concurrent behaviours. We demonstrate how this general set-up works for combined order structures which are based on two relations, viz. an acyclic ‘before’ relation and a possibly cyclic ‘not later than’ relation.

Special Issue Dedicated to Jetty Kleijn on the Occasion of

Reaction systems were introduced in order to provide an abstract model for the study of the biochemical processes that take place in the living cell.Processes of this kind are the result of the interactions between reactions and may be influenced by the environment.Thus, reaction systems can be considered as a model of (interactive) computation.In previous works, various equivalences defined directly on reaction systems and processes had been proposed and compared.These equivalences were all based on functional equivalence that compares a system's behaviour at every stage of its execution.In this paper, in contrast, we investigate enabling equivalence which focuses on the system behaviour only in specific stages of its evolution, namely those where all of its reactions are active.We discuss the effect of such an approach and, in particular, its relationship to a transition system representation of the system's behaviour.

A representation of interval orders by sequences of antichains is discussed, and its relationship to the Fishburn’s representation by sequences of the beginnings and endings of domain elements is analysed in detail. Moreover, an operational semantics based on sequences of maximal antichains is prop osed and investigated for a general class of safe Petri nets with context arcs.

In this paper, we further develop a recently introduced semantic link between temporal logics and Petri nets. We focus on two specific formalisms, Interval Temporal Logic (ITL) and Box Algebra (BA), which are closely related by their compositional approach to constructing system descriptions. The overall goal of our investigation is to translate Petri nets into behaviourally equivalent logical formulas. As a result, the analysis of system properties can be carried out using either of the two formalisms, exploiting their respective strengths and powerful tool support. The contribution of this paper is twofold. First, we extend the existing translation from BA to ITL, by removing restrictions concerning the way control flow of concurrent system is modelled, and by allowing a fully general synchronisation operator. Second, we strengthen the notion of equivalence between a Petri net and the corresponding logical formula by proving such an equivalence at the level of transition-based executions of Petri nets rather than just by looking at their labels. We also show that the complexity of the proposed translation compares favourably with the complexity of the translation from BA expressions to Petri nets.

In the study of behaviours of concurrent systems, traces are sets of behaviourally equivalent action sequences. Traces can be represented by causal partial orders. Step traces, on the other hand, are sets of behaviourally equivalent step sequences, each step being a set of simultaneous actions. Step traces can be represented by relational structures comprising non-simultaneity and weak causality. In this paper, we propose a classification of step alphabets as well as the corresponding step traces and relational structures representing them. We also explain how the original trace model fits into the overall framework.

Reversible computation deals with mechanisms for undoing the effects of actions executed by a dynamic system. This paper is concerned with reversibility in the context of Petri nets which are a general formal model of concurrent systems. A key construction we investigate amounts to adding ‘reverse’ versions of selected net transitions. Such a static modification can severely impact on the behaviour of the system, e.g., the problem of establishing whether the modified net has the same states as the original one is undecidable. We therefore concentrate on nets with finite state spaces and show, in particular, that every transition in such nets can be reversed using a suitable set of new transitions.

This special issue marks the 60th birthday of Professor Gabriel Ciobanu.It consists of 7 original contributions from colleagues who have accompanied Gabriel through his scientific life in one way or another, be it in joint projects, research articles, or even the writing of complete books.We would like to thank all the contributors to this special issue for their hard work and

A step trace is an equivalence class of step sequences, where the equivalence is determined by dependencies between pairs of actions expressed as potential simultaneity and sequentialisability. Step traces can be represented by invariant structures with two relations: mutual exclusion and (possibly cyclic) weak causality. An important issue concerning invariant structures is to decide whether an invariant structure represents a step trace over a given step alphabet. For the general case this problem has been solved and an effective decision procedure has been proposed. In this paper, we restrict the class of order structures being considered with the aim of achieving a better characterisation. Requiring that the weak causality relation is acyclic, makes it possible to solve the problem in a purely local way, by considering pairs of events, rather than whole structures.

A step trace is an equivalence class of step sequences which can be thought of as different observations of the same underlying concurrent history. Equivalence is determined on basis of a step alphabet that describes the relations between events in terms of potential simultaneity and sequentialisab ility. Step traces cannot be represented by standard partial orders, but require so-called invariant structures, extended order structures that capture the phenomena of mutual exclusion and weak causality. In this paper, we present an effective way of deciding whether an invariant structure represents a step trace over a given step alphabet. We also describe a method by which one can check whether a given invariant structure can represent a step trace over any step alphabet. Moreover, if the answer is positive, the method provides a suitable step alphabet.

Reaction systems are a formal model for computational processes inspired by the functioning of the living cell. This paper introduces reaction systems with discrete concentrations, which are an extension of reaction systems allowing for quantitative modelling. We demonstrate that although reaction systems with discrete concentrations are semantically equivalent to the original qualitative reaction systems, they provide much more succinct representations in terms of the number of entities being used. We define a variant of Linear Time Temporal Logic interpreted over models of reaction systems with discrete concentrations. We provide its suitable encoding in SMT, together with bounded model checking, and present experimental results demonstrating the scalability of the verification method for reaction systems with discrete concentrations.

The design and analysis of concurrent computing systems is often concerned with fundamental behavioural properties involving system activities, e.g., boundedness, liveness, and persistence. This paper is about the latter property and a complementary property of nonviolence. Persistence means that an enabled activity cannot be disabled, whereas nonviolence means that executing an activity does not disable any other enabled activity. Since its introduction in the 1970s, persistence has been investigated assuming that each system activity is a single atomic action, but in the design of Globally Asynchronous Locally Synchronous (GALS) systems one also needs to allow activities represented by steps, each step being a set of simultaneously executed atomic actions. Dealing with step based execution semantics creates a wealth of new fundamental problems and questions. In particular, there are different ways in which the standard notion of persistence (and nonviolence) could be lifted to the level of steps. We provide a rich classification of different types of step based persistence and nonviolence. We first do this for a general model of (step) transition systems. After that, we focus on Petri nets, and introduce a taxonomy of persistent and nonviolent steps and markings. We also characterise key structural properties of persistence and nonviolence, linking these behavioural notions with the presence of self-loops in Petri nets.

Both Petri nets and differential equations are important modeling tools for biological processes. In this paper we demonstrate how these two modeling techniques can be combined to describe biological gradient formation. Parameters derived from partial differential equation describing the process of gradient formation are incorporated in an abstract Petri net model. The quantitative aspects of the resulting model are validated through a case study of gradient formation in the fruit fly.

We introduce a process algebra with processes able to migrate between different explicit locations of a distributed environment defined by a number of distinct locations. We use timing constraints over local clocks to control migration and communication, together with local maximal concurrency in the way actions are executed. Two processes may communicate if they are present at the same location and, in addition, they have appropriate access permissions to communicate over a shared channel. Access permissions can be acquired or lost while moving from one location to another. Timing constraints coordinate and control both communication between processes and migration between locations. We completely characterize the situations in which a process is guaranteed to possess safe access permissions in all possible environments. In this way, one can design systems in which processes are not blocked (deadlocked) due to the lack of dynamically changing access permissions.

Abstract The process algebras Timed Mobility (TiMo) and its extension Permissions, Timers and Mobility (PerTiMo) were recently proposed to support engineering applications in distributed system design.TiMoprovides a formal framework in which process migration between distinct locations and timing constraints linked to local clocks can be modelled and analysed. This is extended inPerTiMoby associating access permissions to communication to model security aspects of a distributed system. In this paper we develop a new semantic model forTiMousing Rewriting Logic (RL) and strategies, with the aim of providing a foundation for tool support; in particular, strategies are used to capture the locally maximal concurrent step of aTiMospecification which previously required the use of action rules based on negative premises. This RL model is then extended with access permissions in order to develop a new semantic model forPerTiMo. These RL semantical models are formally proved to be sound and complete with respect to the original operational semantics on which they were based. We present examples of how the developed RL models forTiMoandPerTiMocan be implemented within the strategy-based rewriting systemElanand illustrate the range of (behavioural) properties that can be analysed using such a tool.

A concurrent system is persistent if throughout its operation no activity which became enabled can subsequently be prevented from being executed by any other activity. This is often a highly desirable (or even necessary) property; in particular, if the system is to be implemented in hardware. Over the past 40 years, persistence has been investigated and applied in practical implementations assuming that each activity is a single atomic action which can be represented, for example, by a single transition of a Petri net. In this paper we investigate the behaviour of GALS (Globally Asynchronous Locally Synchronous) systems in the context of VLSI circuits. The specification of a system is given in the form of a Petri net. Our aim is to re-design the system to optimise signal management, by grouping together concurrent events. Looking at the concurrent reachability graph of the given Petri net, we are interested in discovering events that appear in ‘bundles’, so that they all can be executed in a single clock tick. The best candidates for bundles are sets of events that appear and re-appear over and over again in the same configurations, forming ‘persistent’ sets of events. Persistence was considered so far only in the context of sequential semantics. In this paper, we move to the realm of step based execution and consider not only steps which are persistent and cannot be disabled by other steps, but also steps which are nonviolent and cannot disable other steps. We then introduce a formal definition of a bundle and propose an algorithm to prune the behaviour of a system, so that only bundled steps remain. The pruned reachability graph represents the behaviour of a re-engineered system, which in turn can be implemented in a new Petri net using the standard techniques of net synthesis. The proposed algorithm prunes reachability graphs of persistent and safe nets leaving bundles that represent maximally concurrent steps.

Non-interleaving semantics of concurrent systems is often expressed using posets, where causally related events are ordered and concurrent events are unordered. Each causal poset describes a unique concurrent history, i.e., a set of executions, expressed as sequences or step sequences, that are consistent with it. Moreover, a poset captures all precedence-based invariant relationships between the events in the executions belonging to its concurrent history. However, concurrent histories in general may be too intricate to be described solely in terms of causal posets. In this paper, we introduce and investigate generalised mutex order structures which can capture the invariant causal relationships in any concurrent history consisting of step sequence executions. Each such structure comprises two relations, viz. interleaving/mutex and weak causality. As our main result we prove that each generalised mutex order structure is the intersection of the step sequence executions which are consistent with it.

Federated cloud systems increase the reliability and reduce the cost of computational support to an organization. However, the resulting combination of secure private clouds and less secure public clouds impacts on the security requirements of the system. Therefore, applications need to be located within different clouds, which strongly affects the information flow security of the entire system. In this paper, the entities of a federated cloud system as well as the clouds are assigned security levels of a given security lattice. Then a dynamic flow sensitive security model for a federated cloud system is proposed within which the Bell-La Padula rules and cloud security rule can be captured. As a result, one can track and verify the security information flow in federated clouds. Moreover, an example is used to explain how Petri nets could be used to represent such a system, making it possible to verify secure information flow in federated clouds using the existing Petri net techniques.

New technologies influence and change social attitudes by making electronic data easy to use and easy to carry, and this capability impacts data security in business organizations. Therefore, organizations have to define appropriate controls aimed at preventing the loss or leaking of data. Having said that, the effectiveness of security controls in complex dynamic environments has not yet been systematically analyzed. In this paper, we propose a formal system model for data resources in a dynamic environment, which can represent the location of different classes of data resources as well as their users. Using such a model, the concurrent and probabilistic behaviour of the system can be analyzed. This study provides a systematic way of exploring the efficiency of a given security policy, or access control technology, in the business process context. The proposed approach can help a technical expert to develop a deeper analysis of the specific security measures required by a business organization.

A concurrent history represented by a causality structure that captures the intrinsic, invariant dependencies between its actions, can be interpreted as defining a set of closely related observations (e.g., step sequences). Depending on the relations

In membrane systems, biochemical reactions taking place in the compartments of a cell are abstracted to evolution rules that specify which and how many objects are consumed and produced. The recently proposed reaction systems also investigate processes carried by biochemical reactions, but the resulting computational model is remarkably different. A key difference is that in reaction systems, biochemical reactions are modeled using a qualitative rather than a quantitative approach. In this paper, we introduce so-called set membrane systems, a variant of membrane systems with qualitative evolution rules inspired by reaction systems. We then relate set membrane systems to Petri nets which leads to a new class of Petri nets: set-nets with localities. This Petri net model provides a faithful match with the operational semantics of set membrane systems.

One of the possible ways of constructing concurrent systems is their automated synthesis from behavioural specifications. In this paper, we look at a particular instance of this approach which aims at constructing GALS (globally asynchronous locally synchronous) systems from specifications given in terms of transition systems with arcs labelled by steps of executed actions. GALS systems are represented by Elementary Net Systems with Localities (ENL-systems), each locality defining a set of co-located actions. The synthesis procedure is based on the regions of transition systems and we provide a number of criteria aimed at generating a minimal set of regions (conditions) of an ENL-system generating a given transition system.

The unconstrained step semantics of Petri nets is impractical for simulating and modelling applications. In the past, this inadequacy has been alleviated by introducing various flavours of maximally concurrent semantics, as well as priority orders. In this paper, we introduce a general way of controlling step semantics of Petri nets through step firing policies that restrict the concurrent behaviour of Petri nets and so improve their execution and modelling features. In a nutshell, a step firing policy disables at each marking a subset of enabled steps which could otherwise be executed. We discuss various examples of step firing policies and then investigate the synthesis problem for Petri nets controlled by such policies. Using generalised regions of step transition systems, we provide an axiomatic characterisation of those transition systems which can be realised as reachability graphs of Petri nets controlled by a given step firing policy. We also provide two different decision and synthesis algorithms for PT-nets and step firing policies based on linear rewards of steps, where the reward for firing a single transition is either fixed or it depends on the current net marking. The simplicity of the algorithms supports our claim that the proposed approach is practical.

This paper introduces the concept of a 'structured occurrence net', which as its name indicates is based on that of an 'occurrence net', a well-established formalism for an abstract record that represents causality and concurrency information concerning a single execution of a system. Structured occurrence nets consist of multiple occurrence nets, associated together by means of various types of relationship, and are intended for recording or predicting, either the actual behaviour of complex systems as they communicate and evolve, or evidence that is being gathered and analysed concerning their alleged past behaviour. We provide a formal basis for the new formalism and show how it can be used to gain better understanding of complex fault-error-failure chains (i) among co-existing communicating systems, (ii) between systems and their sub-systems, and (iii) involving systems that are controlling, creating ormodifying other systems. We then go on to discuss how, with appropriate tools support, perhaps using extended versions of existing tools, structured occurrence nets could form a basis for improved techniques of system failure prevention and analysis.

Abstract We propose a finite structural translation of possibly recursive π -calculus terms into Petri nets. This is achieved by using high-level nets together with an equivalence on markings in order to model entering into recursive calls, which do not need to be guarded. We view a computing system as consisting of a main program ( π -calculus term) together with procedure declarations (recursive definitions of π -calculus identifiers). The control structure of these components is represented using disjoint high-level Petri nets, one for the main program and one for each of the procedure declarations. The program is executed once, while each procedure can be invoked several times (even concurrently), each such invocation being uniquely identified by structured tokens which correspond to the sequence of recursive calls along the execution path leading to that invocation.

Summary form only given. A new method, algorithms and tool for the visualisation of a finite complete prefix (FCP) of a Petri net (PN) or a signal transition graph are presented. A transformation is defined that converts such a prefix into a two-level model. At the top level, it has a finite state machine (FSM), describing modes of operation and transitions between them. At the low level, there are marked graphs, which can be drawn as waveforms, embedded into the top level nodes. The models of both levels are abstractions traditionally used by electronics engineers. The resultant model is completed trace equivalent to the original prefix. Moreover, the branching structure of the latter is preserved as much as possible.

The paper presents a new method for checking unique and complete state coding, the crucial conditions in the synthesis of asynchronous control circuits from signal transition graphs (STGs). The method detects state coding conflicts in an STG using its partial order semantics (unfolding prefix) and an integer programming technique. This leads to huge memory savings compared to methods based on reachability graphs, and also to significant speedups in many cases. In addition, the method produces execution paths leading to an encoding conflict. Finally, the approach is extended to checking the normalcy property of STGs, which is a necessary condition for their implementability using gales whose characteristic functions, are monotonic.

In the formal treatment of concurrent computing systems, causality and weak causality can be used to provide abstract specifications of the temporal ‘earlier than’ and ‘not later than’ orderings. In this paper we consider relational structures comprising causality and weak causality — called stratified order structures — which can be used to provide a non-sequential semantics of Petri nets with inhibitor arcs. We show that this approach can be extended to nets augmented with priority specifications. In particular, we demonstrate how to derive stratified order structures for such nets by generalising the standard construction of causal partial orders based on occurrence nets.

Abstract This paper studies the correctness of distributed systems made up of replicated processes that communicate by message passing. Processes are described within the divergence model of CSP. The notion of correctness introduced is based on a relation that formally expresses the conformance of an implementation process with the target process it is intended to implement. A weak and a strong version of the relation are introduced, aimed at treating acyclic and cyclic process networks respectively. Both allow the study of (total) correctness and may cope with non-deterministic targets and implementations. We then show how a target process may be implemented (in the formal sense introduced) by replicating it in a set of copies, a majority of which is non-faulty.

The authors present a novel formal approach to proving the correctness of distributed systems of replicated processes that communicate by message passing. The notion of correctness introduced is based on the consistency of the replicated system with its nonreplicated counterpart. The formal framework of CSP (communicating sequential processes) allows the proof of partial correctness and deadlock-freedom properties of the systems of replicated processes. The authors also discuss how a replicated process may be implemented by N-base copies, a majority of which are non-faulty, and point out the necessity of coordinating the copies and the requirements they should satisfy.>