Search

• Investigated efficiency of synthesis of elementary net systems with localities. • Evaluated experimentally different synthesis algorithms. • Investigated theoretically and experimentally finding of unknown localities. 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. [ABSTRACT FROM AUTHOR]

Reaction systems are a model of interactive computation, where the interaction between a system — itself built up of a number of reactions — and its environment is modelled through context sequences provided by the environment. The standard execution semantics of reaction systems is synchronous, i.e., at each computational step all the enabled reactions are executed. In this paper, we 'de-synchronise' such an execution model by allowing only a subset of enabled reactions to be executed. We then study the resulting asynchronous model assuming two fundamental execution policies. The first one allows any subset of reactions to be executed, and the second one draws each subset from a pre-defined pool. We also introduce and discuss the notion of persistence of reactions and sets of reactions in the resulting models of asynchronous reaction systems. In particular, we demonstrate that reaction persistence can be implemented. [ABSTRACT FROM AUTHOR]

Machine Learning (ML) and Internet of Things (IoT) are complementary advances: ML techniques unlock the potential of IoT with intelligence, and IoT applications increasingly feed data collected by sensors into ML models, thereby employing results to improve their business processes and services. Hence, orchestrating ML pipelines that encompass model training and implication involved in the holistic development lifecycle of an IoT application often leads to complex system integration. This article provides a comprehensive and systematic survey of the development lifecycle of ML-based IoT applications. We outline the core roadmap and taxonomy and subsequently assess and compare existing standard techniques used at individual stages. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

Reaction systems originated as models of interactions between biochemical reactions in the living cell. Since then they were also successfully developed as models of interactive computation. Here, the interaction between a (reaction) system and its environment is modelled through context sequences provided by the environment – they influence the processes in the system. In this paper we introduce and investigate a 'plug-in' methodology for providing context sequences, where we view interactive processes from the perspective of the environment. The environment is modelled by a plug-in device, where a reaction system can be plugged in. When a reaction system is plugged in, then it receives context sequences from the plug-in device. Several sorts of such devices are investigated and compared (as influencers of behaviours of reaction systems). [ABSTRACT FROM AUTHOR]

Biology is 3D. Therefore, it is important to be able to analyze phenomena in a spatiotemporal manner. Different fields in computational sciences are useful for analysis in biology; i.e. image analysis, pattern recognition and machine learning. To fit an empirical model to a higher abstraction, however, theoretical computer science methods are probed. We explore the construction of empirical 3D graphical models and develop abstractions from these models in L-systems. These systems are provided with a profound formalization in a grammar allowing generalization and exploration of mathematical structures in topologies. The connections between these computational approaches are illustrated by a case study of the development of the lactiferous duct in mice and the phenotypical effects from different environmental conditions we can observe on it. We have constructed a workflow to get 3D models from different experimental conditions and use these models to extract features. Our aim is to construct an abstraction of these 3D models to an L-system from features that we have measured. From our measurements we can make the productions for an L-system. In this manner we can formalize the arborization of the lactiferous duct under different environmental conditions and capture different observations. All considered, this paper illustrates the joint of empirical with theoretical computational sciences and the augmentation of the interpretation of the results. At the same time, it shows a method to analyze complex 3D topologies and produces archetypes for developmental configurations. [ABSTRACT FROM AUTHOR]

We present the theory of distributed Markov chains (DMCs). A DMC consists of a collection of communicating probabilistic agents in which the synchronizations determine the probability distribution for the next moves of the participating agents. The key feature of a DMC is that the synchronizations are deterministic, in the sense that any two simultaneously enabled synchronizations involve disjoint sets of agents. Using our theory of DMCs we show how one can analyze the behavior using the interleaved semantics of the model. A key point is, the transition system which defines the interleaved semantics is—except in degenerate cases—not a Markov chain. Hence one must develop new techniques to analyze these behaviors exhibiting both concurrency and stochasticity. After establishing the core theory we develop a statistical model checking procedure which verifies the dynamical properties of the trajectories generated by the the model. The specifications consist of Boolean combinations of component-wise bounded linear time temporal logic formulas. We also provide a probabilistic Petri net representation of DMCs and use it to derive a probabilistic event structure semantics. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

Network controllability focuses on the concept of driving the dynamical system associated to a directed network of interactions from an arbitrary initial state to an arbitrary final state, through a well-chosen set of input functions applied in a minimal number of so-called input nodes. In earlier studies we and other groups demonstrated the potential of applying this concept in medicine. A directed network of interactions may be built around the main known drivers of the disease being studied, and then analysed to identify combinations of drug targets controlling survivability-essential genes in the network. This paper takes the next step and focuses on patient data. We demonstrate that comprehensive protein-protein interaction networks can be built around patient genetic data, and that network controllability can be used to identify possible personalised drug combinations. We discuss the algorithmic methods that can be used to construct and analyse these networks. [ABSTRACT FROM AUTHOR]

Some multi-agent scenarios call for the possibility of evaluating specifications in a richer domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of an infinite path, inconsistency analysis in distributed databases, and verification methods that use incomplete anytime algorithms, such as bounded model checking. In this paper, we present multi-valued alternating-time temporal logic (mv-ATL → ∗ ), an expressive logic to specify strategic abilities in multi-agent systems. It is well known that, for branchingtime logics, a general method for model-independent translation from multi-valued to two-valued model checking exists. We show that the method cannot be directly extended to mv-ATL → ∗ . We also propose two ways of overcoming the problem. Firstly, we identify constraints on formulas for which the model-independent translation can be suitably adapted. Secondly, we present a model-dependent reduction that can be applied to all formulas of mv-ATL → ∗ . We show that, in all cases, the complexity of verification increases only linearly when new truth values are added to the evaluation domain. We also consider several examples that show possible applications of mv-ATL → ∗ and motivate its use for model checking multi-agent systems. [ABSTRACT FROM AUTHOR]

For a family of sets we consider elements that belong to the same sets within the family as companions. The global dynamics of a reactions system (as introduced by Ehrenfeucht and Rozenberg) can be represented by a directed graph, called a transition graph, which is uniquely determined by a one-out subgraph, called the 0-context graph. We consider the companion classes of the outsets of a transition graph and introduce a directed multigraph, called an essential motion, whose vertices are such companion classes. We show that all one-out graphs obtained from an essential motion represent 0-context graphs of reactions systems with isomorphic transition graphs. All such 0-context graphs are obtained from one another by swapping the outgoing edges of companion vertices. [ABSTRACT FROM AUTHOR]

Denote by ш the operation of interleaving, or shuffling, of words. We prove that, given a regular language R and a letter-to-letter morphism φ, it is undecidable whether or not there exists a word ω such that ω ш φ(ω) ∩ R ≠ ø. [ABSTRACT FROM AUTHOR]

It is well known that the set of powers of any given order, for example squares, in a regular language need not be regular. Nevertheless, finite automata can identify them via their roots. More precisely, we recall that, given a regular language L, the set of square roots of L is regular. The same holds true for the nth roots for any n and for the set of all nontrivial roots; we give a concrete construction for all of them. Using the above result, we obtain decision algorithms for many natural problems on powers. For example, it is decidable, given two regular languages, whether they contain the same number of squares at each length. Finally, we give an exponential lower bound on the size of automata identifying powers in regular languages. Moreover, we highlight interesting behavior differences between taking fractional powers of regular languages and taking prefixes of a fractional length. Indeed, fractional roots in a regular language can typically not be identified by finite automata. [ABSTRACT FROM AUTHOR]

A transition t stops a place/transition Petri net if each reachable marking of the net enables only finite occurrence sequences without occurrences of t (i.e., every infinite occurrence sequence enabled at this marking contains occurrences of t). Roughly speaking, when t is stopped then all transitions of the net stop eventually. This contribution shows how to identify stoptransitions of unbounded nets using the coverability graph. Furthermore, the developed technique is adapted to a more general question considering a set of stop-transitions and focussing on a certain part of the net to be stopped. Finally, an implementation of the developed algorithm is presented. [ABSTRACT FROM AUTHOR]

Computing a mapping between two process models is a crucial technique, since it enables reasoning and operating across processes, like providing a similarity score between two processes, or merging different process variants to generate a consolidated process model. In this paper we present a new flexible technique for process model mapping, based on the relaxation labeling constraint satisfaction algorithm. The technique can be instantiated so that different modes are devised, depending on the context. For instance, it can be adapted to the case where one of the mapped process models is incomplete, or it can be used to ground an adaptable similarity measure between process models. The approach has been implemented inside the open platform NLP4BPM, providing a visualization of the performed mappings and computed similarity scores. The experimental results witness the flexibility and usefulness of the technique proposed. [ABSTRACT FROM AUTHOR]

When a Petri net is synthesised from a labelled transition system, it is frequently desirable that certain additional constraints are fulfilled. For example, in circuit design, one is often interested in constructing safe Petri nets. Targeting such subclasses of Petri nets is not necessarily computationally more efficient than targeting the whole class. For example, targeting safe nets is known to be NP-complete while targeting the full class of place/transition nets is polynomial, in the size of the transition system. In this paper, several classes of Petri nets are examined, and their suitability for being targeted through efficient synthesis from labelled transition systems is studied and assessed. The focus is on choice-free Petri nets and some of their subclasses. It is described how they can be synthesised efficiently from persistent transition systems, summarising and streamlining in tutorial style some of the authors' and their groups' work over the past few years. [ABSTRACT FROM AUTHOR]

We formalise and study multi-agent timed models MAPTs (Multi-Agent with Periodic timed Tasks), where each agent is associated with a regular timed schema upon which all possible actions of the agent rely. MAPTs allow for an accelerated semantics and a layered structure of the state space, so that it is possible to explore the latter dynamically and use heuristics to greatly reduce the computation time needed to address reachability problems. We use an available tool for the Petri net implementation of MAPTs, to explore the state space of autonomous vehicle systems. Then, we compare this exploration with timed automata-based approaches in terms of expressiveness of available queries and computation time. [ABSTRACT FROM AUTHOR]

Uncertain sequences are compact representations of sets of similar strings. They highlight common segments by collapsing them, and explicitly represent varying segments by listing all possible options. A generalized degenerate string (GD string) is a type of uncertain sequence. Formally, a GD string Ŝ is a sequence of n sets of strings of total size N, where the ith set contains strings of the same length ki but this length can vary between different sets. We denote by W the sum of these lengths k0, k1,... , kn-1. Our main result is an (N + M)-time algorithm for deciding whether two GD strings of total sizes N and M, respectively, over an integer alphabet, have a non-empty intersection. This result is based on a combinatorial result of independent interest: although the intersection of two GD strings can be exponential in the total size of the two strings, it can be represented in linear space. We then apply our string comparison tool to devise a simple algorithm for computing all palindromes in Ŝ in (min{W, n2}N)-time. We complement this upper bound by showing a similar conditional lower bound for computing maximal palindromes in Ŝ. We also show that a result, which is essentially the same as our string comparison linear-time algorithm, can be obtained by employing an automata-based approach. [ABSTRACT FROM AUTHOR]

Techniques to discover Petri nets from event data assume precisely one case identifier per event. These case identifiers are used to correlate events, and the resulting discovered Petri net aims to describe the life-cycle of individual cases. In reality, there is not one possible case notion, but multiple intertwined case notions. For example, events may refer to mixtures of orders, items, packages, customers, and products. A package may refer to multiple items, multiple products, one order, and one customer. Therefore, we need to assume that each event refers to a collection of objects, each having a type (instead of a single case identifier). Such object-centric event logs are closer to data in real-life information systems. From an object-centric event log, we want to discover an object-centric Petri net with places that correspond to object types and transitions that may consume and produce collections of objects of different types. Object-centric Petri nets visualize the complex relationships among objects from different types. This paper discusses a novel process discovery approach implemented in PM4Py. As will be demonstrated, it is indeed feasible to discover holistic process models that can be used to drill-down into specific viewpoints if needed. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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 proposed and investigated for a general class of safe Petri nets with context arcs. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]