Ebook: A Mosaic of Computational Topics: from Classical to Novel

This special issue is dedicated to Jetty Kleijn on the occasion of her 65th birthday. Her research is of broad scope. She made significant contributions to a number of research areas both through solving challenging problems and through pioneering new research directions.

She has published influential papers in:

• classical foundations of computer science, in particular in formal languages and automata theory,

• theory of concurrency, in particular in the area of Petri nets, and

• natural computing, in particular in bio-inspired computing and computational modelling of bio-processes.

A considerable part of her research is of an interdisciplinary character. This includes modelling of specific biological processes using approaches already established in computer science (such as Petri nets) as well as investigating novel models of information processing in bio-systems (such as reaction systems).

She has greatly contributed to the development of scientific communities on both the international and the national (local) level. For example, she is a respected community leader in the area of Petri nets and she played a key role in the formation and functioning of the computer science department (Leiden Institute of Advanced Computer Science) at Leiden University, The Netherlands. She is also passionately engaged in promoting the involvement of women in computer science.

Jetty is well-recognised by the scientific community, which was also demonstrated by the enthusiastic response to our invitation to contribute to this special issues, which (after a thorough refereeing process) resulted in the 14 papers that constitute this special issue. They explore a number of research topics that are either directly or indirectly related to research directions pursued by Jetty.

Comparable to going from P/T Petri nets to coloured Petri nets, in “Discovering Object-centric Petri Nets”, van der Aalst and Berti show how to automatically discover object-centric Petri nets from object-centric event logs in order to visualise the complex relationships among objects from different types. Such object-centric event logs can be seen as an intermediate format closer to the actual data collected by today’s information systems. This novel process discovery approach is implemented in the open-source process mining platform PM4Py.

Generalised degenerate (GD) strings are compact representations of sets of similar strings, for which interest has recently grown, as they can be used to represent pan-genomes. In “Comparing Degenerate Strings”, Alzamel et al. present a linear time algorithm for deciding whether two GD strings have a non-empty intersection, even though the intersection of two GD strings can be exponential in the total size of the two strings. They also apply their string comparison tool to devise a simple algorithm to efficiently compute all palindromes in a GD string.

In “Dynamic Exploration of Multi-agent Systems with Periodic Timed Tasks”, Arcile et al. introduce MAPTs, multi-agent systems composed of periodic communicating autonomous agents evolving in a constrained environment, and study methods tailored for efficient model checking. They use an available tool for the high-level Petri net implementation of MAPTs to explore the state space of communicating autonomous vehicle systems. They also compare such explorations with timed automata-based approaches in terms of expressiveness of available queries and computation time.

In “Target-oriented Petri Net Synthesis”, Best et al. categorise various classes of arc-weighted P/T Petri nets with respect to their suitability for being synthesised efficiently from labelled transition systems. As stipulated by applications from hardware design and synthesis, the focus is on efficient synthesis techniques under the additional restriction that the resulting net should be a choice-free Petri net or some specific subclass. This results in a comprehensive comparison of some of the authors’ and their groups’ work over the past few years.

The automated comparison of process models, which are fundamental for precise representations of organisational processes, has received significant attention in the domain of business process management (BPM). In “Flexible Process Model Mapping using Relaxation Labeling”, Carmona et al. present a flexible novel technique for process model mapping, based on the relaxation labelling constraint satisfaction algorithm. Their approach is implemented in the NLP4BPM open platform, providing visualisations of the performed mappings and computed similarity scores.

For some applications of P/T Petri nets it is relevant to know whether a transition of a net is a stop-transition, which is the case if each reachable marking of the net enables only finite occurrence sequences without occurrences of that transition. In “Stop-transitions of Petri Nets”, Desel and Finthammer show how to identify stop-transitions of unbounded nets using coverability graphs. They moreover adapt their technique to more general questions considering sets of transitions and focussing on certain parts of the net. The developed algorithm is implemented in the Cycl↻n tool to visualise relevant behavioural structures.

It is well known that most natural properties of regular languages are algorithmically decidable. In “Roots and Powers in Regular Languages: Recognizing Nonregular Properties by Finite Automata”, Frei et al. provide an example of a natural property with a surprisingly different behaviour, namely a problem that is non-regular yet identifiable by finite automata. Moreover, they prove that the roots of a regular language, while always regular, may have a state complexity that increases exponentially and they provide concrete constructions for upper and lower bounds on this state complexity.

The global dynamics of reaction systems can be represented by (directed) transition graphs that are uniquely determined by so-called 0-context graphs. In “Companions and an Essential Motion of a Reaction System”, Genova et al. consider companion classes of the outsets of a transition graph and introduce an essential motion as a directed multigraph whose vertices are such companion classes. They observe that all reaction systems whose 0-context graphs are associated to a given essential motion have isomorphic transition graphs. As a result, all such 0-context graphs are related by swapping the outgoing edges of companion vertices.

The operation of shuffling (words) has a long history in the theory of formal languages. In “On Shuffling a Word with its Letter-to-Letter Substitution”, Halava et al. consider a kind of self-shuffle with respect to a letter-to-letter morphism, according to which a word is shuffled with its own image under that letter-to-letter morphism. They prove that, given a regular language and a letter-to-letter morphism, it is undecidable whether or not there exists a word such that the intersection of the self-shuffle of that word with respect to the letter-to-letter morphism and the regular language is empty.

Multi-agent scenarios sometimes require the evaluation of specifications in rich domains of truth values. In “Multi-valued Verification of Strategic Ability”, Jamroga et al. present a multi-valued variant of alternating-time temporal logic, in which the truth values are taken from an arbitrary distributive lattice. They show that multi-valued verification can usually be performed by means of efficient (polynomial-time) translations to classical (2-valued) verification. They also present an appealing case study of drones patrolling for pollution in a city that demonstrates the modelling value of their approach and well as its efficiency.

The theory of traces has a long history in concurrency theory and their algebraic structures and properties are well developed. This is not the case for step traces, which are generalisations of classical traces, and neither for interval traces, which are specialised traces for dealing with interval order semantics. In “Algebraic Structure of Step Traces and Interval Traces”, Janicki and Mikulski define and discuss a number of algebraic aspects (focussing in particular on various types of canonical forms and projection representations) of both step traces and interval traces, with the aim of better understanding their mutual relationship.

Precision medicine aims to integrate patient data with genetic knowledge to find suitable personal therapeutic strategies. In “Network Controllability Analysis of Three Multiple-myeloma Patient Genetic Mutation Datasets”, Sanchez Martin and Petre demonstrate the applicability of network controllability for identifying possible personalised drug combination therapies based on directed networks of protein-protein interactions built around patient genetic data. They discuss the algorithmic methods that can be used to construct and analyse such networks.

In “A Theory of Distributed Markov Chains”, Thiagarajan and Yang present a theory of distributed Markov chains, which are networks of sequential agents synchronising on common actions that determine the probabilistic outcomes. Since the transition systems defining their interleaved semantics are generally not Markov chains, they develop novel statistical model-checking procedures to analyse their behaviour exhibiting a mix of concurrency and stochasticity. They also provide a probabilistic Petri net representation and use it to derive a probabilistic event structure semantics.

In “L-systems from 3D-imaging of Phenotypes of Arborized Structures”, Verbeek and Cao explore the use of L-systems to support the analysis of phenotypes in molecular developmental biology in a spatio-temporal manner through the construction of empirical 3D graphical models and abstractions from these models formalised as L-systems. They illustrate their approach with a case study in which they formalise the arborisation of the lactiferous duct in newborn mice as an L-system, and show how this spatial abstraction enables to represent the phenotypical effects from different environmental conditions as observed from experiments.

The editors and contributors to this special issue wish Jetty happiness and satisfaction in both her personal and scientific life.

We thank the authors and the referees for their efforts to produce this special issue. We are grateful to the editor-in-chief of Fundamenta Informaticae, Professor Damian NiwiÂťnski, for the help and support during the editorial process.

Guest editors:

Maurice ter Beek

ISTI–CNR, Pisa, Italy

Maciej Koutny

Newcastle University, Newcastle upon Tyne, United Kingdom

Grzegorz Rozenberg

Leiden University, Leiden, The Netherlands

The University of Colorado Boulder, Boulder, Colorado, USA

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.

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 k_i but this length can vary between different sets. We denote by W the sum of these lengths k₀, k₁, …, k_n-1. Our main result is an O(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 O(min{W, n²}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.

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.

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.

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.

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 stop-transitions 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.

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.

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.

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 w such that w ⧢ ϕ(w) ∩ R ≠ ∅.

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 branching-time 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.

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.

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.

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.

Biology is 3D. Therefore, it is important to be able to analyze phenomena in a spatio-temporal 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.