Abstract A reaction system consists of a background set of entities and a set of reactions. Reactions are specified by three sets of entities: reactants, inhibitors, and products. A reaction is enabled by a state (a subset of entities), if all its reactants are present in that state and none of its inhibitors. The result of a set of reactions on a given state is a new state that consists of the products of the reactions that were enabled at the original state. In this paper, we further investigate enabling equivalence. This relation equates two sets of reactions for which the states that enable all their reactions simultaneously, are the same and, moreover, their results on those states are the same. From the point of view of enabling equivalence, sets of reactions act as if they were a single (combined) reaction. We show how combined reactions characterize enabling equivalence classes. Furthermore, enabling equivalence induces a partial order in the form of a cover relation on its equivalence classes. The resulting partially ordered set turns out to be a lattice and we demonstrate how this lattice relates to the enabling cover relation introduced earlier for single reactions.

Reaction systems are a computational model originally introduced to formalize the interactions between biochemical reactions that are the basis of the functioning of the living cell. Subsets of reactions of a reaction system define result functions which leads to a concept of functional equivalence. This equivalence in turn induces a functional cover relation on the reactions of a reaction system which captures redundancies in the system. In this paper, the functional cover relation is transferred to functional equivalence classes of sets of reactions. We introduce so-called atoms as building blocks of reactions. Atoms provide a characterization of functional equivalence classes of sets of reactions and are used to prove that the functional cover relation on functional equivalence classes of sets of reactions is a lattice.

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.

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.

Software engineers want to be real engineers.Real engineers use mathematics.Formal methods are the mathematics of software engineering.Therefore, software engineers should use formal methods."Mike HollowayThe Working Formal Methods Symposium (FROM) aims to bring together researchers and practitioners who work on formal methods by contributing new theoretical results, methods, techniques, and frameworks, and/or make the formal methods to work by creating or using software tools that apply theoretical contributions.FROM

This special issue is based on extended versions of the best papers presented at the 39th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2018).Petri Nets 2018 was co-located with the Application of Concurrency to System Design Conference (ACSD 2018).Both were organized by the Interes Institute and Faculty of Electrical Engineering and Information Technology, Slovak University of Technology.The conference took place at the Austria Trend Hotel Bratislava, from June 24 to June 29, 2018.In total, 33 papers were submitted to Petri Nets 2018 by authors from 19 different countries.Each paper was reviewed by three reviewers.The Program Committee (PC) selected 23 papers for presentation: 15 theory papers and 8 tool papers.The authors of the best six papers were invited to submit an extended version of their conference paper for this special issue.The selected papers contained highly innovative and very strong contributions, as was demonstrated by the unanimous support of the reviewers.Also the PC unanimously supported these invitations.After a rigorous review process comprising two rounds of reviewing, the invited papers were accepted.Besides a subset of the original reviewers, we also invited additional reviewers to ensure the best feedback possible.We believe that the papers in this special issue are of high quality and represent the state-of-the-art in their respective fields.The article "Analysis and Synthesis of Weighted Marked Graph Petri Nets" by Raymond Devillers and Thomas Hujsa focuses on an important subclass of persistent Petri nets, the weighted marked graphs (WMGs), also called generalised (or weighted) event (or marked) graphs or weighted T-nets.The authors provide new behavioural properties of WMGs expressed on their reachability graph, notably backward persistence and strong similarities between any two sequences sharing the same starting state and the same destination state.They also propose necessary structural conditions that must be fulfilled by a labelled transition system to be WMG-solvable.Finally, the authors propose a general synthesis method to create a WMG whose reachability graph minimally includes the specification.The article "Operational Semantics, Interval Orders and Sequences of Antichains" by Ryszard Janicki and Maciej Koutny introduces a new general class of nets that can represent both inhibitor and activator nets -called safe nets with context arcs.The authors analyse in detail fundamental relationships between interval sequences and sequences of maximal antichains, and provide simple algorithms that transform one into another.

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.

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.

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.

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.

This special issue is dedicated to selected papers from the 33rd International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2012), which took place in June 2012 in Hamburg, Germany.In a careful reviewing process, 18 regular papers have been accepted for presentation at the conference among 55 submissions.Then, after the conference, a collection of papers published in the proceedings was selected with the help of the Program Committee members, and the authors were invited to revise and extend their contributions for this special issue.Next, the extended submissions have been examined in another independent reviewing process involving two review rounds to meet the standards of FUNDAMENTA INFORMATICAE.Finally, six contributions have been accepted for publication.The accepted papers give a good overview of some recent developments in the area of Petri nets and concurrency.In the article "Old and New Algorithms for Minimal Coverability Sets" by Antti Valmari and Henri Hansen it is presented and proven correct a simple algorithm for computing minimal coverability sets for Petri nets.The features and performance of this algorithm, which is not based on future pruning, are discussed and compared with other approaches based on pruning.It is shown, using examples, that neither approach is systematically better than the other.This paper received the "Outstanding Paper" award at the conference.The paper "A Sweep-Line Method for Büchi Automata-based Model Checking" by Sami Evangelista and Lars Michael Kristensen proposes and experimentally evaluates an algorithm for Büchi automata-based model checking compatible with the search order and with the on-the-fly deletion of states as performed by the sweep-line method.In the paper "Safety and soundness for Priced Resource-Constrained Workflow nets" María Martos-Salgado and Fernando Rosa-Velardo extend workflow Petri nets with discrete prices, by associating a price with the execution of a transition and to the storage of tokens.They develop a framework in which to study safety and soundness for price resource-constrained workflow nets and study the decidability and the complexity of these properties.In the paper "Complexity of the Soundness Problem of Workflow Nets" by GuanJun Liu, Jun Sun, Yang Liu, and JinSong Dong, it is proven that the soundness problem is PSPACE-hard for workflow nets and PSPACE-complete for bounded workflow nets and then also for bounded workflow nets with reset or inhibitor arcs.Additionally, it is proven that the soundness problem is co-NP-hard for asymmetric-choice workflow nets, a larger class than free-choice workflow nets.The paper "Process Discovery and Conformance Checking Using Passages" by W.M.P. van der Aalst and H.M.W. Verbeek proposes an approach to decompose process v v-vi

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.

Motivated by different ways to obtain team automata from synchronizing component automata, we consider various definitions of synchronized shuffles of words. A shuffle of two words is an interleaving of their symbol occurrenceswhich preserves the original order of these occurrences within each of the two words. In a synchronized shuffle, however, also two occurrences of one symbol, each from a different word, may be identified as a single occurrence. In case at least one of the words involved is infinite, a (synchronized) shuffle can also be unfair in the sense that an infinite word may prevail fromsome point onwards even when the other word still has occurrences to contribute to the shuffle. We prove that for the synchronized shuffle operations under consideration, every (fair or unfair) synchronized shuffle can be obtained as a limit of synchronized shuffles of the finite prefixes of the words involved. In addition, it is shown that with the exception of one, all synchronized shuffle operations that we consider satisfy a natural notion of associativity, also in case of unfairness. Finally, using these results, some compositionality results for team automata are established.