jeudi 18 mai, 14h en salle Aurigny
Combining Free choice and Time in Petri Nets
Time Petri nets (TPNs) are a classical extension of Petri nets with timing constraints attached to transitions, for which most verification problems are undecidable. We consider TPNs under a strong semantics with multiple enabling of transitions. We focus on a structural subclass of unbounded TPNs, where the underlying untimed net is free choice, and show that it enjoys nice properties in the timed setting under a multi-server semantics. In particular, we show that the questions of firability (whether a chosen transition can fire), and termination (whether the net has a non-terminating run) are decidable for this class. We then consider the problem of robustness under guard enlargement, i.e., whether a given property is preserved even if the system is implemented on an architecture with imprecise time measurement. This question was studied for TPNs, and decidability of several problems was obtained for bounded classes of nets. We show that robustness of fireablity is decidable for unbounded free choice TPNs with a multi-server semantics. Joint work with S. Akshay and R. Phawade.
Exposés des semaines suivantes
jeudi 1er juin, 14h en salle Aurigny
Laurie Ricker (Mount Allisson University)
Parity Architectures for Discrete-Event Systems
Existing decentralized decision-making architectures for diagnosis and control (that operate in the absence of communication between diagnosers) use either disjunction or conjuction to combine decisions of the local diagnosers or controllers in reaching an overall conclusion about whether or not a fault occurred or when to disable an event. The observational property of interest for languages in this architecture is more generally referred to as inference diagnosability or inference observability. We propose a parity-based architecture that uses XOR, which can be used for both diagnosis and control, to extend the current decision-making capabilities of decentralized agents. A new family of languages that lie beyond those that are inference-diagnosable or inference observable is defined. Finally, a verification algorithm for this new observational property is provided. This is joint work with Finn Lidbetter (Mount Allison) and Herve Marchand.
jeudi 8 juin, 14h en salle Aurigny
Compositional proofs in differential dynamic logic
Modularity and composability are essential properties to facilitate and scale the design of cyber-physical systems from the specification of hybrid, discrete and continuous, components. Modularity is essential to break down a system model into comprehensible and manageable component specifications. Composability is essential to design a system from component models while preserving their verified properties, expressed as assume-guarantee contracts. I will present our recent results which address the specification of hybrid system using Platzer's differential dynamic logic. We define a new composition operator in differential dynamic logic and prove that it is associative and commutative. Plus, we provide a theorem which characterizes necessary conditions to automate the proof that composed components satisfy the composition of their individual contracts, enabling modular and compositional verification. We case-study our composition operator by considering the modular and detailed specification of a cruise controller in KeYmaera X. (Joint work with Jean-Pierre Talpin and Benoit Boyer)
jeudi 15 juin, 14h en salle Aurigny
The Complexity of Diagnosability and Opacity Verification for Petri Nets
Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues. We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions. Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.
Vendredi 30 juin, 14h en salle Aurigny
The Parameterized Complexity of Positional Games
We study the parameterized complexity of several positional games. Our main result is that Short Generalized Hex is W -complete parameterized by the number of moves. This solves an open problem from Downey and Fellows’ influential list of open problems from 1999. Previously, the problem was thought of as a natural candidate for AW[*] -completeness. Our main tool is a new fragment of first-order logic where universally quantified variables only occur in inequalities. We show that model-checking on arbitrary relational structures for a formula in this fragment is W -complete when parameterized by formula size. We also consider a general framework where a positional game is represented as a hypergraph and two players alternately pick vertices. In a Maker-Maker game, the first player to have picked all the vertices of some hyperedge wins the game. In a Maker-Breaker game, the first player wins if she picks all the vertices of some hyperedge, and the second player wins otherwise. In an Enforcer-Avoider game, the first player wins if the second player picks all the vertices of some hyperedge, and the second player wins otherwise. Short Maker-Maker, Short Maker-Breaker, and Short Enforcer-Avoider are respectively AW[*] -, W -, and co-W -complete parameterized by the number of moves. This suggests a rough parameterized complexity categorization into positional games that are complete for the first level of the W -hierarchy when the winning condition only depends on which vertices one player has been able to pick, but AW[*] -complete when it depends on which vertices both players have picked. However, some positional games with highly structured board and winning configurations are fixed-parameter tractable. We give another example of such a game, Short k-Connect, which is fixed-parameter tractable when parameterized by the number of moves. This is joint work with Édouard Bonnet, Serge Gaspers, Antonin Lambilliotte, and Stefan Rümmele (ICALP 2017). Bio: Abdallah Saffidine is an ARC DECRA Fellow and a Research Associate at the University of New South Wales, Sydney, Australia. He works in the Artificial Intelligence and Algorithms groups. He arrived at UNSW in 2013 as a postdoc with Pr. Michael Thielscher and obtained his PhD from the Universite Paris-Dauphine, France, under the supervision of Pr. Tristan Cazenave. Abdallah has a wide range of interests from games, planning, and other areas of decision-making to logic, complexity and other areas of theory.