Overview (in progress)

PN and ACSD sessions schedule

For the scientific program of the workshops, see their respective webpages.

Wednesday, 24th

  • 8:30 – 9:00: Welcome (in front of Forum A and Forum B)
  • 9:00 – 9:30: Opening session (Forum A)
  • 9:30 – 10:30: Invited talk: Robert Lorenz - Modeling Quantitative Aspects of Concurrent Systems using Weighted Petri Net Transducers (Forum A). Session chair: Jörg Desel. Abstract
  • 10:30 – 11:00: Coffee break
  • 11:00 – 12:30: PN session: Analysis (Forum A, in parallel with an ACSD session). Session chair: Piotr Chrzastowski-Wachtel.
    • Marvin Triebel and Jan Sürmeli: Characterizing Stable Inequalities of Petri Nets.
    • Thomas Hujsa, Jean-Marc Delosme and Alix Munier Kordon: On the Reversibility of Live Equal-Conflict Petri Nets.
    • Dario Bruneo, Francesco Longo, Marco Scarpa, Antonio Puliafito, Rahul Ghosh and Kishor Trivedi: An SRN-based Resiliency Quantification Approach.
  • 11:00 – 12:30: ACSD session: Model Checking (Forum B, in parallel with a PN session). Session chair: Jean-François Raskin.
    • Tobias Isenberg: Incremental Inductive Verification of Parameterized Timed Systems
    • Antti Valmari: Stop It, and Be Stubborn!
    • Ala Eddine Ben Salem and Mohamed Graiet: Combining Explicit and Symbolic LTL Model Checking Using Generalized Testing Automata
  • 12:30 – 14:30: Lunch
  • 14:30 – 15:30: Invited talk: Marlon Dumas - Process Mining Reloaded: Event Structures as a Unified Representation of Process Models and Event Logs (Forum A). Session chair: Wil van der Aalst. Abstract
  • 15:30 – 16:00: Coffee break
  • 16:00 – 17:30: PN session: Agents and cooperation (Forum A, in parallel with an ACSD session). Session chair: Robin Bergenthum.
    • Javier Esparza and Jörg Desel: Negotiation Programs.
    • Thomas Wagner and Daniel Moldt: Workflow Management Principles for Interactions between Petri Net-based Agents.
    • Wil van der Aalst, Anna Kalenkova, Eric Verbeek and Vladimir Rubin: Process Discovery Using Localized Events.
  • 16:00 – 17:30: ACSD session: Semantics (Forum B, in parallel with a PN session). Session chair: Stefan Haar.
    • Ferenc Bujtor and Walter Vogler: Testing Preorders for dMTS: Deadlock- and the New Deadlock-/Divergence-Testing
    • Stefan Vijzelaar and Wan Fokkink: Multi-Valued Abstraction Using Lattice Operations
    • Loïc Hélouët, Béatrice Berard and John Mullins: Non-interference in partial order models
  • 18:00 – 20:00 Tool presentation session and reception at the UAE (Alumni association). Click here for the list of tools presented during the session.

Thursday, 25th

  • 09:00 – 10:00: Invited talk: Andrew Brown - SpiNNaker: a neural simulation engine (Forum A). Session chair: Alex Yakovlev. Abstract
  • 10:00 – 10:30: Coffee break
  • 10:30 – 12:00: Joint PN and ACSD session: Tools and applications (Forum A). Session chair: Fabrice Kordon.
    • Monika Heiner, Martin Schwarick and Jan-Thierry Wegener: Charlie – an Extensible Petri Net Analysis Tool.
    • Franck Pommereau: SNAKES, a Flexible High-Level Petri Nets Library.
    • Jaime Arias, Myriam Desainte-Catherine and Camilo Rueda: A Framework for Composition, Verification and Real-Time Performance of Multimedia Interactive Scenarios.
  • 12:00 – 13:30: Lunch
  • 13:30 – 15:00: ACSD session: Processors (Forum B) Session chair: Keijo Heljanko.
    • Qi Tang, Twan Basten, Marc Geilen, Sander Stuijk and Ji-Bo Wei: Task-FIFO Co-Scheduling of Streaming Applications on MPSoCs with Predictable Memory Hierarchy.
    • Alessandro de Gennaro, Paulius Stankaitis and Andrey Mokhov: A Heuristic Algorithm for Deriving Compact Models of Processor Instruction Sets.
    • Ashur Rafiev, Fei Xia, Alexei Iliasov, Rem Gensh, Ali Aalsaud, Alexander Romanovsky and Alex Yakovlev: Order Graphs and Cross-layer Parametric Significance-driven Modelling.
  • 16:00 – 17:00 Social event: visit to the museum of musical instruments (more info to come).
  • 19:30 – ?? Conference banquet at the museum of musical instruments.

Friday, 26th

  • 9:00 – 10:00: Invited talk: Marta Kwiatkowska - On quantitative modelling and verification of DNA walker circuits using stochastic Petri nets (Forum A). Session chair: Jetty Kleijn. Abstract
  • 10:00 – 10:30: Coffee break
  • 10:30 – 12:00: PN session: Complexity (Forum A, in parallel with an ACSD session). Session chair: Serge Haddad.
    • Loïc Hélouët, Éric Badouel and Christophe Morvan: Petri nets with semi-structured data.
    • Nicolas David, Claude Jard, Didier Lime and Olivier Roux: Discrete Parameters in Petri Nets.
    • András Vörös, Àkos Hajdu and Tamas Bartha: New search strategies for the Petri net CEGAR approach.
  • 10:30 – 12:00: ACSD session: Verification (Forum B in parallel with a PN session). Session chair: Roland Meyer.
    • Antti Tapani Siirtola, Stavros Tripakis and Keijo Heljanko: When Do We (Not) Need Complex Assume-Guarantee Rules?
    • Hernan Ponce-De-Leon, Olli Saarikivi, Kari Kähkönen, Keijo Heljanko and Javier Esparza: Unfolding based Minimal Test Suites for Testing Multithreaded Programs.
    • Edmundo López Bóbeda, Maximilien Colange and Didier Buchs: Building a Symbolic Model Checker from Formal Language Description.
  • 12:00 – 14:00: Lunch
  • 14:00 – 15:30: Joint PN and ACSD session: Net extensions, part I (Forum A). Session chair: Lars Kristensen.
    • Hubert Garavel: Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets.
    • Thomas Chatain, Stefan Haar, Maciej Koutny and Stefan Schwoon: Non-Atomic Transition Firing in Contextual Nets.
    • Mohammed Alqarni and Ryszard Janicki: On Interval Process Semantics of Petri Nets with Inhibitor Arcs.
  • 15:30 – 16:00: Coffee break
  • 16:00 – 17:00: Joint PN and ACSD session: Net extensions, part II (Forum A). Session chair: Lars Kristensen.
    • Étienne André, Thomas Chatain and César Rodríguez: Preserving Partial Order Runs in Parametric Time Petri Nets.
    • Hanifa Boucheneb and Kamel Barkaoui: Strongly generalized soundness of Time Workflow Nets.
  • 17:00 – 17:30: Closing session (Forum A).

Invited talks

SpiNNaker – a neural simulation engine, Prof. Andrew Brown, Southampton, UK.

Abstract: SpiNNaker is a completely novel kind of computing architecture, which bears little or no resemblance to Turings original concept of sixty years ago. It was intended, designed and optimised for the problem of neural simulation, but on a scale and at a speed unattainable with conventional machines. The headline goal is to be able to simulate the behaviour of a billion neurons in real time, using a million conventional cores. As neural ensembles become ever more complex, amongst the technical challenges facing the human experimenter is that of interpreting the output: a billion time histories is a formidable mass of data to mine. Received neuroscience wisdom says that the best way to study the high-level behaviour of a large neural ensemble is to embed it in a virtual reality environment, where complex emergent behaviour can be (relatively) easily identified and manipulated. To achieve this requires that the simulation is capable of reacting to stimuli in real time, and this is just what SpiNNaker is designed to do.

In this talk, we present a brief outline of the architecture of the machine, followed by a more detailed description of the specialised approach used within it to integrate (neural) differential equations - we go on to show how this produces biologically realistic behaviour.

A conventional metric for any simulation system is "How fast does it go?" The design intention for SpiNNaker is that it operates in real time; it will simulate the behaviour of one neuron in the same wallclock time as - we hope - a billion.

Whilst there is no way through Amdahls Law (The proportion of code that cannot be parallelised will ultimately limit the advantages accrued from more processors), the Gustafson-Barsis Law does permit a way around it: (If you can have an arbitrary number of processors, the total amount of work performed by the system may be increased arbitrarily at no extra cost).

This is a programming methodology of immense power, only today becoming a feasible research approach as the effective 'cost' of a core approaches zero.

Two research questions SpiNNaker is intended to illuminate:

  • How can massively parallel computing resources accelerate our understanding of brain function?
  • How can our growing understanding of brain function point the way to more efficient parallel, fault-tolerant computation?

Bio : Professor Brown holds an established chair in Electronics at Southampton, and was head of the ESD (Electronic System Design) research group in the Department of Electronics from 1995 to 2007, building it up from three academic staff (the smallest engineering group) to thirteen academic staff (the largest engineering group) in that period. He has worked as a Visiting Scientist at IBM Hursley Park (UK) and Siemens Munich (Germany), MAC Communications as part of the Senior Academics in Industry program, and has held Visiting Chair positions at the Universities of Trondheim (Norway), Cambridge (UK); and Ecole Polytechnique Federale de Lausanne (Switzerland).

He has been involved in three spin-outs, all as a founding director: Horus Systems Ltd (1985) - electronic system simulation, LME Design Automation (2000) - electronic system synthesis (where he was awarded a two-year Royal Society Industrial Fellowship) and ECSPartners (2003) - a consultancy company set up to oversee and coordinate external consultancy activities in ECS.

He is a Fellow of the BCS and the IET, a Senior Member of the IEEE, a UK Chartered Engineer (CEng) and the EU equivalent (Eur Ing).

Process Mining Reloaded: Event Structures as a Unified Representation of Process Models and Event Logs, Prof. Marlon Dumas, Tartu, Estonia.

Abstract: Process mining is a family of methods to analyze event logs produced during the execution of business processes in order to extract insights regarding their performance and conformance with respect to normative or expected behavior. The landscape of process mining methods and use cases has expanded considerably in the past decade. However, the field has evolved in a rather ad hoc manner without a unifying foundational theory that would allow algorithms and theoretical results developed for one process mining problem to be reused when addressing other related problems. In this talk we will advocate a foundational approach to process mining based on a well-known model of concurrency, namely event structures. We outline how event structures can serve as a unified representation of behavior captured in process models and behavior captured in event logs. We then sketch how process mining operations, specifically automated process discovery, conformance checking and deviance mining, can be recast as operations on event structures.

Bio: Marlon Dumas is Professor of Software Engineering at University of Tartu, Estonia. Prior to this appointment he was faculty member at Queensland University of Technology and visiting researcher at SAP Research, Australia. His research interests span across the fields of software engineering, information systems and business process management. His ongoing work focuses on combining data mining and formal methods for analysis and monitoring of business processes. He has published extensively in conferences and journals across the fields of software engineering and information systems. He is co-inventor of six granted US/EU patents and co-author of two textbooks in the field of business process management.

On quantitative modelling and verification of DNA walker circuits using stochastic Petri nets, Prof. Marta Kwiatkowska, Oxford, U.K.

Abstract: Molecular programming is an emerging field concerned with building synthetic biomolecular computing devices at the nanoscale, for example from DNA or RNA molecules. The appeal of these devices is their autonomy, in the sense of being able to sense and react unaided to the biochemical environment, and programmability, that is, they can be configured to perform a given task. Many promising applications have been proposed, ranging from diagnostic biosensors and nanorobots to synthetic biology, but prohibitive complexity and imprecision of experimental observations makes reliability of molecular programs difficult to achieve. This paper advocates the development of design automation methodologies for molecular programming, highlighting the role of quantitative verification and synthesis in this context. We focus on DNA 'walker' circuits, in which molecules can be programmed to traverse tracks placed on a DNA origami tile, taking appropriate decisions at junctions and reporting the outcome when reaching the end of the track. It has been shown recently that DNA walkers can evaluate arbitrary Boolean functions. The behaviour of individual walkers is inherently probabilistic and thus probabilistic model checking methods can be used for their analysis. We demonstrate how DNA walkers can be modelled using stochastic Petri nets, and apply statistical model checking using the tool Cosmos to analyse the reliability and performance characteristics of the designs. The results are compared and contrasted with those obtained for the PRISM model checker. The paper ends by summarising current status and future research challenges in the field.

Bio: Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She led the development of the PRISM model checker (www.prismmodelchecker.org), the leading software tool in the area and widely used for research and teaching. Applications of probabilistic model checking have spanned communication and security protocols, nanotechnology designs, power management, game theory, planning and systems biology, with genuine flaws found and corrected in real-world protocols. Kwiatkowskais research is funded by the ERC Advanced Grant VERIWARE "From software verification to everyware verification" and a £5m EPSRC programme grant on Mobile Robotics. She is a member of Academia Europea and Fellow of the BCS, and in 2014 she was awarded an honorary doctorate from KTH Royal Institute of Technology in Stockholm.q

Modeling Quantitative Aspects of Concurrent Systems using Weighted Petri Net Transducers, Prof. Dr. Robert Lorenz, Augsburg, Germany.

Abstract: We present a basic framework for weighted Petri net transducers (PNTs) for the weighted translation of partial languages (consisting of partial words) as a natural generalisation of weighted finite state transducers (FSTs). Weights may represent cost, time consumption or probability of a transition execution. PNTs are a general model to consider such quantitative aspects of process calculi represented by arbitrary partial words. Concerning weights, we use the algebraic structure of concurrent semirings which is based on bisemirings and induces a natural order on its elements. Using the operations of this algebra, the weight of general partial words can be defined in a natural way and turns out to be compositional. As desirable, complex PNTs can be composed from simple PNTs through composition operations like union, product, closure, parallel product and language composition. Composed PNTs yield a compositional computation of weights, except for the case of language composition. For the quick construction of PNTs and evaluation of PNT-algorithms we developed the tool PNTool. PNTool is a python library based on the framework SNAKES allowing for the modular construction of PNTs through composition operations, the visualization of PNTs and weighted partial words, and the simulation of constructed PNTs. We present the algorithms implemented in PNTool and use PNTool to show examples for the application of PNTs in the area of semantic dialogue modeling and natural language processing.

Bio: Robert Lorenz is Professor at the Department of Computer Science of Augsburg University, Germany. Prior to this appointment he was Professor at Eichstätt University, Germany. He holds a Diploma in Mathematics and a PhD in Mathematics from Eichstätt University. His research interests concern the theory of concurrent systems. He is member of the steering committee of the „Special Interest Group on Petri Nets and Related System Models“ of the Gesellschaft für Informatik (GI) and editor of its information service "Petri Net Newsletter".