In a distributed system, in which an action can be either "hidden" or "observable", an unwanted information flow might arise when occurrences of observable actions give information about occurrences of hidden actions. A collection of relations, i.e. reveals and its variants, is used to model such information flow among transitions of a Petri net. This paper recalls the reveals relations defined in [3], and proposes an algorithm to compute them on bounded equal-conflict PT systems, using a smaller structure than the one defined in [3].
Long periods of dry and cold weather conditions significantly increase fire risks for wooden buildings. Recent advances in predictive fire risk models combined with publicly available cloud-based weather data services have enabled the development of smart software systems for location-oriented fire risk notification. We have developed a Coloured Petri Net (CPN) model specifying the software architecture of a microservice-based predictive fire risk notification system. The CPN model captures the set of micro-services provided via REST APIs and the interaction between the constituent services for location tracking and subscription, fire risk computation and data harvesting. As part of the work, we have applied an agile-oriented implementation-first modelling approach and developed a general pattern for REST-based APIs. We apply simulation and state space exploration to validate and verify key behavioural properties of the predictive fire risk notification system.
Recently a new compositional framework for constructing and analysing Boolean networks was presented based on merging entities using Boolean connectives. While this framework provides a good basis for engineering Boolean networks, its practical application is limited by the restricted composition structures allowed and the lack of support for attractor analysis. In this paper we significantly extend this compositional framework by developing a new general structure for compositions and by providing new techniques for compositionally identifying the attractors of a Boolean network. The results presented are important as they support ongoing work to use the framework for engineering biological systems and also provide a new basis for analysing Boolean networks which helps to address the practical limitations imposed by the state space explosion problem.
Elementary Net Systems with Localities (enl-systems) is a class of Petri nets introduced to model gals (globally asynchronous locally synchronous) systems, where some of the components might be considered as logically or physically close and acting synchronously, while others might be considered as loosely connected or residing at distant locations and communicating with the rest of the system in an asynchronous way. The specification of the behaviour of a gals system comes very often in the form of a transition system. The automated synthesis, based on regions, is an approach that allows to construct Petri net models from their transition system specifications. In our previous papers we developed algorithms and tool support for the synthesis of enl-systems from step transition systems, where arcs are labelled by steps (sets) of executed actions. In this paper we focus on the minimisation of the synthesised nets. In particular, we discuss the properties of minimal, companion, and complementary regions, and their role in the process of minimisation of enl-systems. Furthermore, we propose strategies to eliminate redundant regions. Our theoretical results are backed by experiments (the algorithms for the minimisation are implemented within the workcraft framework).
The concurrent places of a Petri net are all pairs of places that may simultaneously have a token in some reachable marking. Concurrent places generalize the usual notion of dead places and are particularly useful for decomposing a Petri net into synchronized automata executing in parallel. We present a state-of-the-art toolchain to compute the concurrent places of a Petri net. This is achieved by a rich combination of various techniques, including: state-space exploration using BDDs, structural rules for concurrent places, quadratic over- and under-approximation of reachable markings, and polyhedral abstraction of the state space based on structural reductions and linear arithmetic constraints on markings. We assess the performance of our toolchain on a large collection of 850 nets originating from the 2022 edition of the Model Checking Contest.
The volume and diversity of healthcare data available using modern technology offers great potential for improving health services delivery. Giving clinicians and health system administrators the ability to easily investigate and analyze data from various perspectives can promote evidence-based decision-making. Current analysis approaches often result in process models where essential relations are difficult to depict and/or discern. Moreover, it is not easy to change the level of detail in order to accommodate user requirements by allowing them to analyze data from various perspectives or capture temporal aspects of the data. Further, inherent differences between patients and the vast variety of healthcare settings, even for one patient, make process mining extremely difficult. In this paper, we first discuss community detection methods which, together with filtering techniques based on dimensional modeling and ontologies, allow us to obtain “contextual” insights from event log data using what we call “contextual process mining”. Then, to capture time-dependent relations in patient data, we propose a linear temporal logic-based language, $$LTL_{EOT}$$ ( $$LTL_{EOT}$$ : Event-Ontology-Time Linear Temporal Logic), which can be used to express both time and order-dependent conditions. The $$LTL_{EOT}$$ formulas are used to filter the event log data to find those patients who satisfy the conditions, thus capturing “temporal” insights in event log data. Both the investigations using community detection methods and those using the temporal logic methods are validated learning approaches: the first allows the user to experiment with the level of abstraction, while the second allows the user to experiment with the temporal logic formulas. This approach can give healthcare professionals insights into patterns of admission, diagnosis, and treatment among patients, which, in turn, lead to the overall goal of this research, which is improved resource management, scheduling, and other aspects of health services delivery. In a simple case study, we show this approach leads to an improved understanding of healthcare processes among comorbid patients.
This paper presents a solution to the issue of how to compute probabilities in nets with confusion, where confusion is interference between concurrent choices of which enabled transition to perform. A formal framework is developed – using a novel formula based on event weights – for computing the probabilities of execution traces of an acyclic net, which in turn are used to compute the probabilities of the markings, steps, and nodes of the net. We prove the framework satisfies generic probability requirements. We also prove the formula simplifies to the standard formula for computing the probability of independent concurrent events in confusion-free concurrent simple acyclic nets with choice, in the maximally concurrent and interleaving models of concurrency.
In this paper we propose a timed abstraction, called acceleration, for the analysis of NCTAs, a class of networks of timed automata tailored to model systems composed out of non-deterministic cyclic agents updating shared variables. The abstraction is based on “maximal action zones”, easy to compute on the fly, which generally aggregate regions in a different way than classical zones do. The original and accelerated semantics are shown coherent in the sense that they both lead to the same untimed semantics, and satisfy the same class of positive reachability queries.
We consider a two-player game on Petri nets, in which each player controls a subset of transitions. The players are called ‘user’ and ‘environment’; we assume that the environment must guarantee progress on its transitions. A play of this game is a run in the unfolding of the net, satisfying the progress assumption. In general, we define a strategy for the user as a map from the set of ‘observations’ to subsets of transitions owned by the user. Different restrictions on strategies can be used to encode observability assumptions. We say that a given strategy is implementable if the net can be endowed with new places so that the runs of the new net coincide with the plays of the original net, complying with the strategy. We propose an algorithm based on the search of regions to decide whether a strategy is implementable.
To improve the treatment of many diseases, continuous monitoring of the patient at home with the ability of doctors to interact with individual cases demands an increasing number of medical devices connected to the cloud. To support the doctor's duties, such devices may benefit from AI-based diagnosis routines. In order for such devices to be approved and placed on the market, they need to comply with various legal, regulatory, economic, and social requirements. An integral part of these requirements is the protection of the patients' data. In this paper, based on a current use case, we describe a workflow on how to identify risks and address their mitigations. To this end, we recall the relevant legal, regulatory, economic, and social data protection requirements. We pursue our findings on a Homecare OCT device that is intended to be used by elderly patients on a daily basis, by taking images of their eyes and sending them for further analysis to a cloud- and AI-based system. The patient's ophthalmologist gets notified for further dedicated treatment depending on the result. To perform the risk management, we describe (i) the architecture of the homecare system, (ii) analyze its data flow, (iii) discuss several vectors of attack, and (iv) propose ways to mitigate the risks.
In our research we study self-adapting multi-agent systems in the context of organisation-oriented design combined with the MAPE pattern (monitor, analyse, plan, and execute). We advocate a models@run.time approach for the planning phase to estimate the cost-benefit ratio of possible self-modifications. In this paper we develop key values to describe the dynamics of self-adapting systems. Our main objective is to compare adaption dynamics of similar systems, i.e., systems that differ only slightly, e.g., w.r.t. their organisational networks. We specify the MAPE-based adaption in the formalism of Hornets – a formalism that uses nets as tokens, i.e., they follow the nets-within-nets approach. We identify abstractions of the reachability graph that focus on the adaption aspects of the processes. We develop key measures for adaption processes on these abstracted graphs. The key measures are used e.g., to compare two variations of the same adapting system. The approach is illustrated by a case study: We analyse a Hornet-model of Axelrod’s well-known tournament where the playing agents adapt their strategies during the game.
With the continued increase of size and complexity of contemporary digital systems, there is a growing need for models of large size and high complexity, as well as methods of analyzing such models. This paper presents a method for simulating large-scale concurrent Petri net models using parallel distributed hardware platforms. By using POETS architecture, our method allows the mapping of concurrent Petri net executions onto 49,152 parallel processing hardware threads to achieve orders of magnitude (45 to 220 times) improvements of simulation speed, compared to conventional simulation methods using single processor systems. The presented method employs techniques including Petri net model partitioning, the use of max-step and locally-interleaving semantics, and the fair firing of transitions.
Thanks to a rich Petri net theory, there exists a broad range of verification techniques for Petri nets. Most of them have a performance that highly depends on the particular combination of net and property. That is why several verification tools for Petri nets use portfolio approaches where various verification algorithms are run concurrently. In this note, we sketch the architecture of a portfolio manager, using the tool LoLA 2.0 as a running example. The portfolio of a verification problem is organized as a task tree. The leafs of the task tree are actual verification algorithms while the inner nodes represent the logical structure of the portfolio. The portfolio manager schedules verification algorithms and assigns resources to them (processor cores, memory, and time). Moreover, it evaluates the consequences of returned results with regard to the original verification problem.
Structural transformations that preserve properties of formal models of concurrent systems make their verification easier. We define structural transformations that allow to abstract and refine elementary net systems. Relations between abstract models and their refinements are formalized using morphisms. Transformations proposed in this paper induce morphisms between elementary net systems as well as preserve their behavioral properties, especially deadlocks. We also show the application of the proposed transformations to the construction of a correct composition of interacting workflow net components.
In the model checking domain the state explosion problem is the core issue. The cause is usually the sheer size of the model or the cardinality of tokens in the initial state. For the latter, which we call token-scaling models, we propose an under-approximation for reachable states. The idea is to reduce the number of tokens in the initial state and thus reducing the state space. If in the reduced state space a witness path is found, then the witness path can also be executed in the original state space. This method preserves existential temporal properties (ECTL∗) using a simulation relation between the reduced and the original state space. Since the cardinality of the initial marking varies from only a few tokens to multi-digit numbers of tokens, we apply heuristics to compute the number of tokens that should be removed. We implemented the new method in the explicit model checker LoLA 2. The experiments, done on the model checking contest benchmark, show that this method can speed up the model checking process and solve additional queries.
We investigate to what extent existing algorithms for the discovery of component models from event logs can be leveraged to a system of asynchronously communicating components. Here, Enterprise nets model local processes, while Industry nets are compositions of Enterprise nets which interact through asynchronous message passing. We investigate the relation between the behaviour of an Industry net and that of its constituting Enterprise nets and we formalise the (causal) structure of global (Industry net) behaviour in terms of a partial order derived from the message passing. Next, we specify how (existing) algorithms for the discovery of isolated processes, can be adapted to enable the discovery of Enterprise nets, and we demonstrate how to combine these Enterprise nets into an Industry net. Using the results on the structure of the global behaviour, we relate the behaviour of the Industry net thus synthesised to the behaviour of the Enterprise nets and show how fitness of the Enterprise nets (the event log provided as input is included in the behaviour of the discovered net) is preserved as fitness of the Industry net. Moreover, we discuss possible underfitting of the global model (the model exhibits more behaviour than observed in the event log) and show how it can be explained in terms of concurrency between the component models and a completeness property of the event log.
Current process discovery techniques are unable to produce meaningful models for semi-structured processes, as they are either too inaccurate or too complex. In this paper we use the idea of local process models (LPMs) to model fragments of a semi-structured process and explore the potential of sets of LPMs. Automatic LPM discovery finds many small patterns but doesn’t find patterns larger than 4–5 events, it produces too many models, and the discovered models describe some events from the log multiple times while leaving others unexplained. We manually construct a set of LPMs for the well-known BPIC12 event log that (1) contains a small number of models that (2) have high accuracy measures such as fitness and precision while (3) they together cover the whole event log and (4) do not cover parts of the log multiple times unnecessarily. We find that existing evaluation techniques for LPMs do not work for sets of LPMs and we propose several measures that help determine the quality of a set of LPMs both as a whole and as individual LPMs. We show that sets of LPMs can indeed be used to model semi-structured processes by not thinking of such processes as monolithic, but rather a collection of smaller processes working together.
The regions of a condition/event transition system can be used to identify the sequential components of the distributed system it represents. With the aim of analysing such a system with respect to its local states, we study the structure obtained from ordering the regions by set inclusion. The resulting algebraic structure is an orthomodular partial order (omp). Given an omp, one can then define another condition/event transition system, canonical with respect to it. We are interested in characterising cases in which an omp is stable, i.e. it is isomorphic to the omp obtained as the regional structure of its canonical transition system. We propose, to this aim, a composition operation, and a refinement operation for stable orthomodular partial orders, the results of which are stable.
Petri nets are an established formal method for modelling and verifying asynchronous, concurrent and distributed systems. To verify a specification, given as a temporal logic formula, state space methods often encounter the state space explosion problem. We propose a verification technique to solve the CTL query E (\( \phi \) U \( \psi \)) using the Petri net state equation with a counterexample guided abstraction refinement (CEGAR) approach. As a side product we show that (EX)\(^{k}\phi \) formulas can be solved with the CEGAR approach as well. We use these special formulas as building bricks to solve the class of finite-linear-path CTL-formulas. The proposed techniques are strong at invalidating infeasible behaviour. In addition to this it will often terminate quickly. We are also introducing quick-checks for solving EG \(\phi \) under certain circumstances.
MQTT is a publish-subscribe communication protocol being increasingly used for implementing internet-of-things (IoT) applications. In earlier work we have developed a formal and executable model of the MQTT protocol using Coloured Petri Nets (CPNs) and performed an initial verification of behavioural properties. The contribution of this paper is to investigate the use of the sweep-line method for verification of the MQTT CPN model in order to alleviate the effect of the state explosion problem. We formulate the behavioural properties using Computation Tree Logic (CTL) and show how to formulate a progress measure for the sweep-line method based on the main phases of the MQTT protocol. To perform the verification of properties, we provide some property-specific CTL model checking algorithms compatible with the sweep-line method.
