Distinguished Carl Adam Petri Lecture
Reasoning about Discovery Clouds
A discovery cloud is a set of automated, cloud-hosted services to which individuals may outsource their routine and not-so-routine research tasks: finding relevant data, inferring links between data, running computational experiments, inferring new knowledge claims, evaluating the credibility of knowledge claims produced by others, designing experiments, and so on. If developed successfully, a discovery cloud can accelerate and democratize access to data and knowledge tools and the collaborative construction of new knowledge. Such systems are also fascinating to consider from a reasoning perspective because they integrate great complexity at multiple levels: the underlying cloud-based hardware and software, for which issues of reliability and responsiveness may be paramount; the knowledge bases and inference engines that sit on that cloud substrate, for which issues of correctness may be less well defined; and the human communities that form around the discovery clouds, and that arguably form as much as part of the cloud as the hardware, software, and data. In this talk I raise questions about what it might mean to reason about such systems. I do not promise any answers.
From Actions, Transactions, and Processes to Services
For the problem domain of business process engineering we introduce, model, and formalize notions of business processes such as action, actor, event, business process, business transaction. In addition, for the solution domain of service-oriented architectures (SOA) we introduce, model, and formalize notions of service, service composition, service-oriented architecture, and layered SOA in a systematic way. We do that by a rigorous mathematical system model. For that purpose, we first develop a basic mathematical system model for formalizing fundamental concepts of processes and services. The goal is to provide a minimal set of formal modeling concepts, nevertheless expressive enough to formalize key notions and concepts in business process engineering and service-oriented architectures capturing also their mutual relationships. This way, the relationship between central notions in business process modeling is captured formally, which provides a basis for a methodology for deriving the systematic specification and design of service-oriented architectures from business process modeling. The purpose of the approach is manifold; one goal is a clear definition of terminology, concepts, terms, and models in business process modeling and SOA; another goal is a rigorous formal basis for the specification, design, and development of business processes and, in particular, SOAs. We end up with a strictly formal concept for the development steps from business process models to services as part of a SOA-oriented development process.
On Processes and Paradigms
Understanding the causal relations between occurrences of actions (events) during a run of a distributed system is crucial for reasoning about its behaviour. We will present a semantical theory for extended Elementary Net (EN) systems based on executions and observations represented as sequences of steps (sets of one or more simultaneously occurring transitions). When step sequences are used to describe a run of an EN system, transitions that can be observed one after the other in any order can also occur together in a step and vice versa. This property reﬂects the ‘true concurrency paradigm’. In this case the structure of runs can be described in terms of partial orders. In general however, the relational structures obtained from sets of step sequences are not partial orders. We characterise the general order structures that correspond to the least restrictive, most general paradigm and that can thus capture any concurrent history consisting of labelled structures underlying the step sequences that form the observations of a run. These structures prove to match exactly with step traces, a generalisation of Mazurkiewicz traces to equivalence classes of step sequences. EN systems with inhibitor arcs and mutex arcs are a system model for the general concurrency paradigm. Their process semantics and step trace semantics ﬁt together through these general order structures. The presentation is based on and extends earlier work done together with Ryszard Janicki, Maciej Koutny, and Łukasz Mikulski
Decidability border for Petri nets with data: WQO dichotomy conjecture
In Petri nets with data, every token carries a data value, and executability
of a transition is conditioned by a relation between data values involved.
Decidability status of various decision problems for Petri nets with data
may depend on the structure of data domain. For instance, if data values
are only tested for equality, decidability status of the reachability
problem is unknown (but decidability is conjectured). On the other hand,
the reachability problem is undecidable if data values are additionally
equipped with a total ordering.
We investigate the frontiers of decidability for Petri nets with various data, and formulate the WQO Dichotomy Conjecture: under a mild assumption, either a data domain exhibits a well quasi-order (in which case one can apply the general setting of well-structured transition systems to solve problems like coverability or boundedness), or essentially all the decision problems are undecidable for Petri nets over that data domain.
The Inevitable Coincidence: A Basis for Concurrency and Distribution
The principle of Propositions as Types is an inevitable coincidence: independently formulated notions of logic and computation turn out to be identical. Under it, propositions correspond to types, proofs to programs, and simpliﬁcation of proofs corresponds to evaluation of programs. It is a robust notion, adapting to almost all areas of computation, but with one important exception: concurrency! I will explain what Propositions as Types means, why it is important, and why concurrency and distribution may at last be about to benefit from this approach. And I will explain how this links to a broader research effort on extending the benefits of types to communication by introducing session types.
- S. Akshay, Blaise Genest and Loic Helouet: Timed-Arc Petri Nets with (restricted) Urgency
- Eike Best and Raymond Devillers: The Power of Prime Cycles
- Eike Best, Evgeny Erofeev, Uli Schlachter and Harro Wimmel: Characterising Petri Net Solvable Binary Words
- Lawrence Cabac, Michael Haustermann and David Mosteller: Renew 2.5 – Towards a Comprehensive Integrated Development Environment for Petri Net-Based Applications
- Thomas Chatain and Josep Carmona: Anti-Alignments in Conformance Checking -- The Dark Side of Process Models
- Leonid Dworzanski and Irina Lomazova: Structural Place Invariants for Analyzing the Behavioral Properties of Nested Petri Nets
- Yrvann Emzivat, Benoît Delahaye, Didier Lime and Olivier H. Roux: Probabilistic Time Petri Nets
- Quentin Gaudel, Pauline Ribot, Elodie Chanthery and Matthew Daigle: Health Monitoring of a Planetary Rover Using Hybrid Particle Petri Nets
- Loic Helouet and Karim Kecir: Realizability of Schedules by Stochastic Time Petri Nets with Blocking Semantics
- Lars Kristensen and Vegard Veiset: Transforming CPN Models into Code for TinyOS: A Case Study of the RPL Protocol
- Franck Pommereau: ABCD: a user-friendly language for formal modelling and analysis
- Uli Schlachter: Petri Net Synthesis in Restricted Classes of Nets
- Jacek Sroka, Andrzej Kierzek and Wojciech Ptak: AB-QSSPN: Integration of agent-based simulation of cellular populations with quasi-steady state simulation of genome scale intracellular networks
- Eric Verbeek and Wil van der Aalst: Merging Alignments for Decomposed Replay
- András Vörös, Dániel Darvas, Vince Molnár, Attila Klenik, Ákos Hajdu, Attila Jámbor, Tamas Bartha and Istvan Majzik: PetriDotNet 1.5: Extensible Petri Net Editor and Analyser for Education and Research
- András Vörös, Vince Molnár, Istvan Majzik, Kristóf Marussy, Miklós Telek and Attila Klenik: Efficient decomposition algorithm for stationary analysis of complex stochastic Petri net models
- Waheed Ahmad, Marijn Jongerden, Mariëlle Stoelinga and Jaco van de Pol: Model Checking and Evaluating QoS of Batteries in MPSoC Dataflow Applications via Hybrid Automata
- Mohammed A. N. Al-hayanni, Ashur Rafiev, Rishad Shafik and Fei Xia: Power and Energy Normalized Speedup Models for Heterogeneous Many Core Computing
- Étienne André, Michał Knapik, Wojciech Penczek and Laure Petrucci: Controlling Actions and Time in Parametric Timed Automata
- Juliana Bowles, Behzad Bordbar and Mohammed Alwanain: Weaving True-Concurrent Aspects using Constraint Solvers
- Ferenc Bujtor and Walter Vogler: ACTL for Modal Interface Automata
- Raymond Devillers: Products of Transition Systems and Additions of Petri Nets
- Martijn Hendriks, Marc Geilen, Amir R. B. Behrouzian, Twan Basten, Hadi Alizadeh and Dip Goswami: Checking Metric Temporal Logic with TRACE (tool paper)
- Mahdi Jelodari Mamaghani, Danil Sokolov and Jim Garside: Asynchronous Dataflow De-Elastisation For Efficient Heterogeneous Synthesis
- Hanna Klaudel, Maciej Koutny and Ben Moszkowski: From Petri Nets with Shared Variables to ITL
- Ondřej Meca, Stanislav Böhm, Marek Běhálek and Petr Jančar: An Approach to Verification of MPI Applications Defined in a High-Level Model
- Dennis Schmitz, Daniel Moldt, Lawrence Cabac, David Mosteller and Michael Haustermann: Utilizing Petri Nets for Teaching in Practical Courses on Collaborative Software Engineering
- Matthew Travers, Rishad Shafik and Fei Xia: Power-Normalized Performance Optimization of Concurrent Many-Core Applications
- Antti Valmari: The Congruences Below Fair Testing with Initial Stability