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.

Process mining provides valuable insights by discovering process models from execution logs.However, its effectiveness depends heavily on high-quality, well-structured logs.Many real-world systems produce low-level, semi-structured logs lacking clear process identifiers, causing misalignment with their intended process models.This paper introduces a method for structuring raw event logs by segmenting event streams and mapping them to known processes.Using process traces from experienced users, we develop a model that infers process assignments in unstructured logs.Our approach is motivated by a modular enterprise system without predefined workflows, where dynamic processes generate low-level logs requiring interpretation.We validate our method on a semi-synthetic business dataset and a fully synthetic dataset from PLG2.Our results demonstrate that trace segmentation improves process discovery, aligns logs with meaningful structures, and significantly enhances process mining in unstructured environments.This work was supported by the Regional Operational Programme of the Kuyavian-Pomeranian Voivodeship for 2014-2020 under the grant titled "Budowa zaplecza badawczo-rozwojowego w MGA Sp. z o.o." variability of clients, the heterogeneity of business processes, and the system's flexibility, incorporating process identifiers into the logs is not feasible from a business perspective.Therefore, our methodology relies exclusively on semi-structured data.By implementing this approach, we provide a solution that enhances process mining capabilities in environments where structured event logs are unavailable.This research contributes to process mining by introducing a method for structuring semi-structured event logs, enabling more effective business process analysis, anomaly detection, and performance monitoring.a) Replication Package: To facilitate reproducibility and further research, we provide a complete replication package containing code, data, and experimental scripts.It is publicly available at:The remainder of this paper is organized as follows.Section II discusses related work.Sections III and IV reviews necessary preliminaries on event logs, process mining, and similarity measures.Section V states the problem, and Section VI describes our methodology for structuring semi-structured event logs.In Section VII, we discuss our experimental design, and Section VIII presents the results.In Section IX, we assess threats to validity.Finally, we conclude and propose future directions in Section X. A. Running Example (Motivation)Consider a customer-support system where each event is logged as [time, user, activity, . ..].A typical log snippet might look like:

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.

In every matured theory, there is a need to investigate possible relationships between considered objects. To address this issue, it is natural to relate a category with given model of computing. Thanks to such approach, many properties are unified and simplified. In this paper, we investigate how category theory can be used to give a faithful semantics for reaction systems. In particular, we propose and discuss possible approaches to the problem of defining morphisms between reaction systems. We provide the definition of morphism that keeps the behaviour of the original reaction system. Especially, some equivalences of reaction systems are reflected in terms of morphisms. For this purpose we expressed isomorphisms and sections in term of transition systems. Moreover, the accelerating morphism defined in the last section gives a new approach for including time in reaction systems.

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.

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)

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.

Traces and their extensions as comtraces, step traces and interval traces are quotient monoids over sequences or step sequences that play an important role in the formal analysis and verification of concurrent systems. Step traces are generalizations of comtraces and classical traces while interval traces are specialized traces that can deal with interval order semantics. The algebraic structures and their properties as projections, hidings, canonical forms and other invariants are very well established for traces and fairly well established for comtraces. For step traces and interval traces they are the main subject of this paper.

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.

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.

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.

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.

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.