| Tuesday, September 6th, 2022 | |||||||
|---|---|---|---|---|---|---|---|
| 19:00-21:00 | Welcome Drink Venue: Building A, 10th Floor | ||||||
| Wednesday, September 7th, 2022 | |||
|---|---|---|---|
| 8:30-8:50 | Arrival of participants & Registration Venue: Building B, Ground Floor, Testbed Control Room | ||
| 8:50-9:50 | Testbed Control Room, Building B, Ground Floor Joerg Raisch. Efficient Consensus over Wireless Channels & and its Use in Traffic Automation Problems. Plenary Session I Chair: Thomas Moor | ||
| 9:50-10:20 | Coffee Break | ||
| 10:20-12:00 | WeAT1-2 Sessions | ||
| Session WeAT1: A-303, Building A, 3rd Floor Invited Session WeAT1 Discrete event systems-based control of mobile agents Chair: Spyros A. Reveliotis; Co-Chair: Kai Cai | Session WeAT2: Testbed Control Room, Building B, Ground Floor Regular Session WeAT2 Security I Chair: Dimitri Lefebvre; Co-Chair: Alessandro Giua | ||
| 10:20-10:40 WeAT1.1 | Young In Kim, Spyros A. Reveliotis*. Some structural results for the problem of Min-Time Coverage in Constricted Environments | 10:20-10:40 WeAT2.1 | Qi Zhang, Carla Seatzu, Zhiwu Li*, Alessandro Giua. Sensor and Actuator Attacks in Discrete Event Systems. |
| 10:40-11:00 WeAT1.2 | Peng Lv, Guangqing Luo, Xiang Yin*, Ziyue Ma, Shaoyuan Li. Optimal Multi-Robot Path Planning for Cyclic Tasks using Petri Nets | 10:40-11:00 WeAT2.2 | Rabah Ammour*, Saïd Amari, Leonardo Brenner, Isabel Demongodin, Dimitri Lefebvre. Observer Design for Labeled Finite Automata with Inputs under Stealthy Actuators Attacks |
| 11:00-11:20 WeAT1.3 | Masahiro Konishi*, Tomotake Sasaki, Kai Cai. Efficient Safe Control via Deep Reinforcement Learning and Supervisory Control — Case Study on Multi-Robot Warehouse Automation | 11:00-11:20 WeAT2.3 | Li Yuting, Christoforos Hadjicostis*, Naiqi Wu. Tamper-Tolerant Diagnosability Under Bounded or Unbounded Attacks |
| 11:20-11:40 WeAT1.4 | Sabino Francesco Roselli*, Remco Vader, Martin Fabian, Knut Akesson. Leveraging Conflicting Constraints in Solving Vehicle Routing Problems | 11:20-11:40 WeAT2.4 | Públio M. Lima, Carlos K. P. Silva, Lilian Kawakami Carvalho, Marcos Vicente Moreira*. Event-based cryptography for automation networks of cyber-physical systems using the stream cipher ChaCha20 |
| 11:40-12:00 WeAT1.5 | Gang Chen*, Yu Lu, Rong Su. Fault tolerance makespan synthesis in multi-process systems via resource sharing and backtracking | 11:40-12:00 WeAT2.5 | Loic Desgeorges*, Jean-Philippe Georges, Thierry Divoux . Detection of cyber-attacks in network control planes using Hidden Markov Model |
| 12:00-13:00 | Lunch Break | ||
| 13:00-14:00 | Testbed Control Room, Building B, Ground Floor Sam Coogan. Specification-Guided Safe Learning using Probabilistic Finite Abstractions Plenary Session II Chair: Spyros A. Reveliotis | ||
| 14:10-15:50 | WeBT1-2 Regular Sessions | ||
| Session WeBT1: A-303, Building A, 3rd Floor Applications I Chair: Elzbieta Roszkowska; Co-Chair: Joanna van de Mortel-Fronczak | Session WeBT2: Testbed Control Room, Building B, Ground Floor Security II Chair: Herve Marchand; Co-Chair: Tomáš Masopust | ||
| 14:10-14:30 WeBT1.1 | Sofia Hustiu*, Cristian Mahulea, Marius Kloetzer. Parallel Motion Execution and Path Rerouting for a Team of Mobile Robots. | 14:10-14:30 WeBT2.1 | Jiří Balun*, Tomas Masopust. On Verification of Weak and Strong k-Step Opacity for Discrete-Event Systems. |
| 14:30-14:50 WeBT1.2 | Jeroen Johannes Verbakel*, Marc Erik Watireza Vos de Wael, Joanna van de Mortel-Fronczak, Wan Fokkink, J.E. Rooda. Supervisory control of roadside units | 14:30-14:50 WeBT2.2 | Crystal Sharpe, Laurie Ricker*, Herve Marchand. Mutual Opacity between Multiple Adversaries |
| 14:50-15:10 WeBT1.3 | Elzbieta Roszkowska*, Piotr Makowski Czerski, Łukasz Janiec. Multi-level control for mobile robot systems. | 14:50-15:10 WeBT2.3 | Qinrui Chen*, Rong Su, Zhiwu Li. Attackable detectability of partially-observed discrete-event systems under sensor attack |
| 15:10-15:30 WeBT1.4 | Martijn Angelo Goorden*, Joanna van de Mortel-Fronczak, Koen van Eldik, Wan Fokkink, J.E. Rooda. Lessons learned in the application of formal methods to the design of a storm surge barrier control system. | 15:10-15:30 WeBT2.4 | Michel Rodrigo das Chagas Alves*, Karen Rudie, Patricia Nascimento Pena. A Security Testbed for Networked DES Control Systems |
| 15:30-15:50 WeBT1.5 | Amaury Beaudet*, Eric Zamai, Cédric Escudero, Emil Dumitrescu. Malicious Origin of Deadlocks in Flexible Manufacturing Systems. | 15:30-15:50 WeBT2.5 | Bohan Cui, Xiang Yin*, Shaoyuan Li, Alessandro Giua. You Don’t Know What I Know: On Notion of High-Order Opacity in Discrete-Event Systems |
| 15:50-16:20 | Coffee Break | ||
| 16:20-18:00 | WeCT1-2 Journal Sessions | ||
| Session WeCT1: A-303, Building A, 3rd Floor Journal I Chair: Tomáš Masopust; Co-Chair: Jan Komenda | Session WeCT2: Testbed Control Room, Building B, Ground Floor Journal II Chair: Sébastien Lahaye; Co-Chair: Kai Cai | ||
| 16:20-16:45 WeCT1.1 | George Jiroveanu, René Boel. From local to global consistency in distributed monitoring of Petri Net models | 16:20-16:45 WeCT2.1 | Hanifa Boucheneb, Kamel Barkaoui, Qian Xing, KuangZe Wang, GaiYun Liu, ZhiWu Li. Time based deadlock prevention for Petri nets |
| 16:45-17:10 WeCT1.2 | Kuize Zhang. Polynomial-time verification and enforcement of delayed strong detectability for discrete-event systems | 16:45-17:10 WeCT2.2 | Teng Long, Qing-Shan Jia. Joint Optimization for Coordinated Charging Control of Commercial Electric Vehicles Under Distributed Hydrogen Energy Supply |
| 17:10-17:35 WeCT1.3 | Jiri Balun, Tomas Masopust. Comparing the notions of opacity for discrete-event systems | 17:10-17:33 WeCT2.3 | Yin Tong, Yucheng Wang, Alessandro Giua. A Polynomial Approach to Verifying the Existence of a Threatening Sensor Attacker |
| 17:35-18:00 WeCT1.4 | Bram van der Sanden, Marc Geilen, Michel Reniers, Twan Basten. Partial-Order Reduction for Supervisory Controller Synthesis | 17:35-18:00 WeCT2.4 | Kai Cai, Alessandro Giua, and Carla Seatzu. Consistent reduction in discrete-event systems |
| 19:00-23:00 | Robo Networking Evening | ||
| 19:00-20:00 | Dinner and Drink at CIIRC | ||
| 20:00-20:40 | Academic Orchestra concert | ||
| 21:00 – 21:30 | WODES 30th Anniversary Ceremony | ||
| 21:30-23:00 | Testbed Tour and networking at robobar | ||
| Thursday, September 8th, 2022 | |||
|---|---|---|---|
| 8:40-9:00 | Arrival of participants & Registration Venue: Building B, Ground Floor, Testbed Control Room | ||
| 9:00-10:00 | Testbed Control Room, Building B, Ground Floor Elżbieta Roszkowska. Automation of control synthesis for mobile robot systems Plenary Session III Chair: Spyros A. Reveliotis | ||
| 10:00-10:30 | Coffee Break | ||
| 10:30-12:30 | ThAT1-2 Sessions | ||
| Session ThA1: Testbed Control Room, Building B, Ground Floor Supervisory Control Theory Chair: Stephane Lafortune; Co-Chair: Thomas Moor | Session ThA2: A-303, Building A, 3rd Floor (Max,+)-algebra Chair: Mehdi Lhommeau; Co-Chair: Sébastien Lahaye | ||
| 10:30-10:50 ThAT1.1 | Lukas Triska, Thomas Moor. Abstraction Based Supervisory Control for Non-Regular ∗-Languages. | 10:30-10:50 ThAT2.1 | Philipp Goltz*, Germano Schafaschek, Laurent Hardouin, Joerg Raisch. Optimal output feedback control of Timed Event Graphs including disturbances in a resource sharing environment |
| 10:50-11:10 ThAT1.2 | Marcelo Rosa*, Jose E. R. Cury, Fabio Baldissera . A Formal Modular Synthesis Approach for the Coordination of Multi-Agent Systems | 10:50-11:10 ThAT2.2 | Davide Zorzenon*, Jan Komenda, Joerg Raisch. Switched Max-Plus Linear-Dual Inequalities: Application in Scheduling of Multi-Product Processing Networks |
| 11:10-11:30 ThAT1.3 | Rômulo Meira-Góes*, Eunsuk Kang, Stephane Lafortune, Stavros Tripakis. On synthesizing tolerable and permissive controllers for labeled transition systems | 11:10-11:30 ThAT2.3 | Germano Schafaschek*, Laurent Hardouin, Joerg Raisch. A Novel Approach for the Modeling and Control of Timed Event Graphs with Partial Synchronization |
| 11:30-11:50 ThAT1.4 | Ana Maria Mainhardt*, Anne-Kathrin Schmuck. Assume-Guarantee Synthesis of Decentralised Supervisory Control. | 11:30-11:50 ThAT2.4 | Jan Komenda*, Davide Zorzenon, Jiří Balun. Modeling of safe timed Petri nets by two-level (max,+) automata |
| 11:50-12:10 ThAT1.5 | Michel Reniers*, Calvin Dingemans. Supervisory control with absent-state explanations for coloured finite automata | 11:50-12:10 ThAT2.5 | Davide Zorzenon*, Germano Schafaschek, Dominik Tirpák, Soraia Moradi, Laurent Hardouin, Joerg Raisch. Implementation of procedures for optimal control of timed event graphs with resource sharing |
| 12:10-12:30 ThAT1.6 | Minqiang Zou, Yin Tong, Ziyue Ma*. PNBA: A Software for Marking Estimation and Reconfiguration in Petri Nets Using Basis Marking Analysis | 12:10-12:30 ThAT2.6 | Guilherme Espindola-Winck*, Renato Markele Ferreira Cândido, Laurent Hardouin, Mehdi Lhommeau. Efficient state-estimation of Uncertain Max-Plus linear systems with high observation noise |
| 12:30-13:30 | Lunch Break | ||
| 13:30-15:30 | ThBT1-2 Regular Sessions | ||
| Session ThBT1: Testbed Control Room, Building B, Ground Floor Verification I Chair: Kai Cai; Co-Chair: Eric Fabre | Session ThBT2: A-303, Building A, 3rd Floor Timed Discrete-Event Systems Chair: Francesco Basile; Co-Chair: Jan Komenda | ||
| 13:30-13:50 ThBT1.1 | Yiheng Tang*, Thomas Moor. Compositional Verification of Non-Blockingness with Prioritised Events | 13:30-13:50 ThBT2.1 | Ibis Velasquez, Euriell Le Corronc*, Yannick Pencolé. Active Diagnosis Algorithm for the Localization of Time Failures in (Max,+)-Linear Systems |
| 13:50-14:10 ThBT1.2 | Takumi Hamada, Shigemasa Takai*. Verification of Reliable Inference-Diagnosability for Decentralized Diagnosis with Single-Level Inference | 13:50-14:10 ThBT2.2 | Rémi Parrot*, Hanifa Boucheneb, Mikaël Briday, Olivier H. Roux. Expressiveness and analysis of Delayable Timed Petri Net |
| 14:10-14:30 ThBT1.3 | Eric Fabre. Resilience in discrete event systems | 14:10-14:30 ThBT2.3 | Sébastien LAHAYE*, Aiwen Lai, Jan Komenda. Weight-deterministic max-plus automata |
| 14:30-14:50 ThBT1.4 | Sander Thuijsman*, Michel Reniers, Kai Cai. Transformational Nonblocking Verification | 14:30-14:50 ThBT2.4 | Camille Coquand*, Audine Subias, Yannick Pencolé, Eric Lubat. Critical pairs based diagnosability analysis of timed fault in Time Petri Nets |
| 14:50-15:10 ThBT1.5 | Dimitri Lefebvre*, Zhiwu Li, Ye Liang. Verifiers for the detection of timed patterns in discrete event systems | 14:50-15:10 ThBT2.5 | Francesco Basile*, Luigi Ferrara. A Matlab toolbox implementing MSCG computation |
| 15:10-15:30 ThBT1.6 | Tianchen Zhang, Kuize Zhang*. Eventual strong detectability of labeled weighted automata over monoids | ||
| 15:30-16:00 | Coffee Break | ||
| 16:00-17:40 | ThCT1-2 Regular Sessions | ||
| Session ThCT1: Testbed Control Room, Building B, Ground Floor Verification II Chair: Joao Carlos Basilio; Co-Chair: Manuel Navarro-Gutiérrez | Session ThCT2: A-303, Building A, 3rd Floor Applications II Chair: Bengt Lennartson ; Co-Chair: Martin Fabian | ||
| 16:00-16:20 ThCT1.1 | José Guilherme Castro, Gustavo Viana, Marcos Vicente Moreira*. Distributed Identification of Discrete-Event Systems with the Aim of Fault Detection | 16:00-16:20 ThCT2.1 | Bengt Lennartson. Reductions and Abstractions for Optimization of Modular Timed Automata |
| 16:20-16:40ThCT1.2 | Antonio Ramirez-Trevino, Carlos Renato Vazquez*, Ian Paniagua, Gerardo Vazquez. Quotient Petri nets | 16:20-16:40 ThCT2.2 | Gaetano Volpe, Maria Pia Fanti*, Agostino Marcello Mangini. Job Shop Sequencing in Manufacturing Plants by Timed Coloured Petri Nets and Particle Swarm Optimization |
| 16:40-17:00ThCT1.3 | Raúl García-Adame, Antonio Ramirez-Trevino*, Carlos Renato Vazquez, Manuel Navarro-Gutiérrez. On liveness analysis in mono-T-semiflow Petri nets based on choice-join pairs | 16:40-17:00 ThCT2.3 | Sahar Mohajerani*, Martin Fabian, Wolfgang Ahrendt. Modeling and Security Verification of State-Based Smart Contracts |
| 17:00-17:20 ThCT1.4 | Braian de Freitas*, Joao Carlos Basilio. Online Fault Diagnosis of Discrete Event Systems Modeled by Labeled Petri Nets Using Labeled Priority Petri Nets | 17:00-17:20 ThCT2.4 | Lars Moormann*, Albert Hofkamp, Joanna van de Mortel-Fronczak, Wan Fokkink, J.E. Rooda. Derivation and Hardware-in-the-loop Testing for a Road Tunnel Controller |
| 17:20-17:40 ThCT1.5 | Ramla Saddem Ramla*, Dylan Baptiste. Machine learning based approach for online fault Diagnosis of Discrete Event System | ||
| Friday, September 9th, 2022 | |||||||
|---|---|---|---|---|---|---|---|
| 9:30-12:30 | Guided Tour of Prague | ||||||
Invited Lectures
Joerg Raisch
Efficient Consensus over Wireless Channels & and its Use in Traffic Automation Problems
Consensus algorithms are routinely employed in a variety of multi-agent scenarios. They require that each agent iteratively evaluates a multivariate function of its neighbours’ information states. If a wireless communication channel is used, this is typically implemented through protocols (such as TDMA – Time Division Multiple Access) that avoid superposition of transmitted signals by assigning each transmitter its own (time) slot.
However, consensus only requires that agents know a function of their neighbours’ information states, not the individual information states. Hence one may ask whether using the famous Kolmogorov-Arnold representation theorem might allow to exploit the channel’s superposition property to drastically reduce communication effort. Kolmogorov-Arnold essentially states that every continuous multivariate function can be expressed via univariate functions and addition. If channel superposition were to be considered as addition, all agents could consequently simultaneously transmit a suitably preprocessed version of their information state, with receiving agents locally postprocessing the received superposition signal.
We will explain for two widely used consensus types (average consensus and max-consensus) why in practice the application of Kolmogorov-Arnold is not quite as straightforward. For both consensus types, we will suggest alternative approaches, which make use of the channel’s superposition property while handling non-ideality effects such as time-varying unknown channel coefficients. By allowing all agents to transmit at the same time, the required number of transmission slots is considerably reduced. In the second part of the talk, we will demonstrate how average and max consensus algorithms can be used in various traffic automation scenarios. This includes platooning, distributed automatic lane changing, and distributed automation of traffic intersections. The reported results are based on joint work with S. Stan
Sam Coogan
Specification-Guided Safe Learning using Probabilistic Finite Abstractions
For stochastic cyber-physical systems subject to a planning specification defined in, e.g., temporal logic, a common approach to control synthesis is to obtain a finite-state abstraction of the dynamics in the form of a Markov Decision Process (MDP) and then apply techniques from probabilistic formal methods to synthesize a control strategy. In many cases, however, the system dynamics are not fully known, and this added degree of uncertainty prevents obtaining a controller that a priori achieves desirable performance. Instead, a control strategy is required that is able to learn the system dynamics in order to ultimately achieve the system specification.
In this talk, we first describe how interval-valued Markov Decision Processes (IMDP) are a natural model for finite-state abstractions of systems subject to uncertain-but-learnable dynamics. Unlike MDPs, IMDPs allow for a range of transition intervals between any two states, and in our setting, this range arises from the uncertain dynamics. We then propose a method that iteratively generates high-confidence IMDP abstractions of a given system from high-confidence bounds on an unknown component of the dynamics obtained via Gaussian process regression. In particular, we develop a specification-guided strategy to sample the unknown dynamics by finding system trajectories that avoid violation of the specification. This iterative learning continues until we obtain a control policy that ultimately achieves the desired planning specification. We apply our methodology to bipedal locomotion planning in an uncertain environment in which motion perturbations from multiple sources of uncertainty are incorporated in a prismatic inverted pendulum model of a bipedal robot.
Elzbieta Roszkowska
Automation of control synthesis for mobile robot systems
The talk is devoted to the hybrid control of multiple mobile robot systems (MMRS), that comprises the supervisory control level, based on a DES approach to modelling MMRS, and the robot control level, based on a continuous time abstraction of the robot motion. We present an overview of the approaches to the development of such systems. The proposed models are defined in a general way, thus enabling an automatic synthesis of the control system for MMRSs with variable number of robots and flexibly assigned missions. It is formally proved that the behaviour of these systems is correct with respect to the defined qualitative criteria. The proposed architecture of the controller allows its application both in a real MMRS and a simulation system for experimental optimization of MMRS operation with respect to quantitative criteria.