Proceedings The 7th International Workshop on
Edited by: Anne Remke and Dung Hoang Tran
Symbolic-Numeric Methods for Reasoning about CPS and IoT
Online, 23rd August 2021
Welcome to the proceedings of the 7th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR 2021). The workshop was planned to take place in Paris, France as a satellite event of QONFEST’21. Due to the COVID-19 pandemic, the whole event took place online. SNR focuses on the combination of symbolic and numeric methods for reasoning about Cyber-Physical Systems and the Internet of Things to facilitate model identification, specification, verification, and control synthesis for these systems. The synergy between symbolic and numerical approaches is fruitful thanks to their complementarity:
- Symbolic methods operate on exact and discrete representations of systems, the set of reachable states, the distribution of model parameters or the possible gains for controller parameters.
- Numeric methods operate on various forms of numerical approximations and continuous transformations of the systems, as developed in the area of continuous dynamical systems and control theory.
The workshop program consisted of three invited talks by Bardh Hoxha (Toyota Research Institute North America, USA), Stanley Bak (Stony Brook University), and Nil Jansen (Radboud University, Netherlands).
The proceedings contain five papers underlying contributed talks. All papers were reviewed by the program committee that consisted of the following members:
- Dung Tran (Co-chair, University of Nebraska-Lincoln, USA)
- Anne Remke (Co-chair, University Münster, Germany)
- Stefan Schupp (TU Wien, Austria)
- Taylor T. Johnson (Vanderbilt University, USA)
- Mario Gleirscher (University of York, UK)
- Erika Ábrahám (RWTH Aachen, Germany)
- Arnd Hartmanns (University of Twente, Germany)
- Ernst Moritz Hahn (University of Twente, Germany)
- Weiming Xiang (Augusta University, USA)
- Gethin Norman (Glasgow University, UK)
- Andreas Rauh (ENSTA Bretagne, Brest, France)
- Goran Frehse (ENSTA Paris, France)
- Stefan Ratschan (Academy of Sciences of the Czech Republic)
- Sofie Haesaert (Eindhoven University of Technology, The Netherlands)
- Thao Dang (CNRS/Verimag, France)
- David Monniaux (CNRS/Verimag, France)
- Milan Češka (Brno University of Technology, Czech Republic)
- Martin Fränzle (Carl von Ossietzky Universit¨at Oldenburg, Germany)
- Luan Viet Nguyen (University of Dayton, USA)
- Chuchu Fan (Massachusetts Institute of Technology, USA)
The organization of SNR 2021 would not have been possible without the combined efforts of many individuals who contributed their share under the difficult circumstances of the COVID-19 pandemic. Especially, we thank the workshop speakers and authors for presenting their research at SNR and the participants for contributing in the discussions. We are grateful to the QONFEST organizers for making the online event run smoothly. Finally, we thank the PC members for their work in ensuring the quality of the contributions, and the SNR Steering Committee: Erika Ábrahám, Sergiy Bogomolov, Martin Fränzle, Taylor T. Johnson and Ashish Tiwari for their advice and support.
Dung Tran (University of Nebraska, Lincoln) and Anne Remke (University of Münster, Germany)
Nils Jansen (Radboud University Nijmegen)
Decision making for modern autonomous systems has to account for various sources of uncertainty. Examples are lossy long-range communication channels with a spacecraft orbiting the earth , or the expected responses of human operators . Moreover, sensor limitations may lead to imperfect information of the current state of the system. Yet, autonomous systems often operate in safety-critical settings. A convenient way to reason about safety is to employ formal verification together with a (partial) model that captures the relevant aspects of a system. Specifically, model checking asserts correctness of a system model [2, 13] regarding specifications such as temporal logic constraints .
Epistemic POMDPs. The standard models to reason about decision-making under uncertainty and imperfect information in artificial intelligence are partially observable Markov decision processes  (POMDPs). With a wide range of POMDP applications, such as robotics [33, 36], humanitarian relief aid , treatment of heart disease , ecology [12, 29], and many more ; scalable approaches to verifiable safety have the potential to render decision-making under uncertainty amenable to safetycritical applications in the real world.
The likelihood of uncertain events, like a message loss in communication channels or of specific responses by human operators, is often only estimated from data. Yet, likelihoods enter a POMDP model as concrete probabilities. POMDPs, in fact, require
precise transition and observation probabilities. Uncertain POMDPs (uPOMDPs)
remove this assumption by incorporating uncertainty sets of probabilities [6
]. These sets are part of the transition and observation model in uPOMDPs and take the form of, for example, probability intervals or likelihood functions [18
]. Such uncertainty is commonly called epistemic
, which is induced by a lack of precise knowledge. Consequently, uPOMDPs are also referred to as epistemic POMDPs.
A spacecraft example. Consider a robust spacecraft motion planning system which serves as decision support for a human operator. This system delivers advice on switching to a different orbit or avoiding close encounters with other objects in space. Existing POMDP models assume that a fixed probability captures the responsiveness of the human . However, a single probability does not faithfully capture the responsiveness of multiple operators. Instead, we use bounds on the actual value of this probability and obtain a uPOMDP model.
Robust policies and neural networks. A policy for the decision support system necessarily considers all potential probability distributions and may need to predict the current location of the spacecraft based on its past trajectory. Therefore, it requires robustness against the uncertainty, and memory to store past (observation) data. The general problem we address is to compute a policy for a uPOMDP that is verifiably robust against all possible probabilities from the uncertainty set. Even without uncertainties, the problem is undecidable .
(a) Memoryless policy.
(b) Five-memory-state policy.
Figure 1: Case study on spacecraft motion planning.
A heuristic approach to enable robustness against uncertainty is to employ neural networks as policy representations for POMDPs. In particular, recurrent neural networks (RNNs) in reinforcement learning settings perform well as either state or value estimators [38
] or as control policies [20
]. Yet, RNNs are complex structures that capture non-linear input-output relations [31
], and providing verifiable guarantees on safety is hard [35
In this talk we present our approaches to compute so-called robust
finite state controllers (FSCs) [30
] that succinctly represent robust policies under verifiable guarantees. Our methods employ recurrent neural networks that are verified and trained within a verification loop that provides counterexamples against safety [24
]. The verification approaches rely on robust convex optimization techniques [4
]. We are able to solve (u)POMDPs with millions of states, which is by far out of reach for the state-of-the-art. We show the applicability of the approaches using two case studies, namely aircraft collision avoidance [27
] and spacecraft motion planning [17
]. Figure 1 shows two instances of the aforementioned
spacecraft problem where (a) the policy (the FSC) has no access to memory or (b) has access to five memory states. The red line shows the spacecraft trajectory based on the computed policy, other indicate potential orbits. The policy without memory (a) needs to switch orbit more often than the policy with five memory nodes (b), and thus consumes more fuel.
This work is based on [37, 16, 10, 7, 9, 8], and the underlying methods rely on [14, 25]. I want to thank all my co-authors for the extremely fruitful collaboration.
Christopher Amato, Daniel S Bernstein & Shlomo Zilberstein (2010):
Optimizing Fixed-size Stochastic Controllers for POMDPs and Decentralized POMDPs.
Christel Baier & Joost-Pieter Katoen (2008):
Principles of Model Checking.
Bram Bakker (2001):
Reinforcement Learning with Long Short-Term Memory.
Available at https://proceedings.neurips.cc/paper/2001/hash/a38b16173474ba8b1a95bcbc30d3b8a5-Abstract.html.
Stephen Boyd & Lieven Vandenberghe (2004):
Cambridge university press,
Raissa Zurli Bittencourt Bravo, Adriana Leiras & Fernando Luiz Cyrino Oliveira (2019):
The Use of UAV s in Humanitarian Relief: An Application of POMDP-Based Methodology for Finding Victims.
Production and Operations Management 28(2),
Brendan Burns & Oliver Brock (2007):
Sampling-Based Motion Planning with Sensing Uncertainty.
Steven Carr, Nils Jansen & Ufuk Topcu (2020):
Verifiable RNN-Based Policies for POMDPs Under Temporal Logic Constraints.
Steven Carr, Nils Jansen & Ufuk Topcu (2021):
Task-Aware Verifiable RNN-Based Policies for Partially Observable Markov Decision Processes.
Journal of Artificial Intelligence Research 72,
Steven Carr, Nils Jansen, Ralf Wimmer, Jie Fu & Ufuk Topcu (2018):
Human-in-the-Loop Synthesis for Partially Observable Markov Decision Processes.
Steven Carr, Nils Jansen, Ralf Wimmer, Alexandru Constantin Serban, Bernd Becker & Ufuk Topcu (2019):
Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks.
Anthony R Cassandra (1998):
A survey of POMDP applications.
In: Working notes of AAAI 1998 fall symposium on planning with partially observable Markov decision processes 1724.
Iadine Chadès, Eve McDonald-Madden, Michael A McCarthy, Brendan Wintle, Matthew Linkie & Hugh P Possingham (2008):
When to stop managing or surveying cryptic threatened species.
Proceedings of the National Academy of Sciences 105(37),
Edmund M Clarke, Thomas A Henzinger, Helmut Veith & Roderick Bloem (2018):
Handbook of model checking 10.
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen & Ufuk Topcu (2021):
Convex Optimization for Parameter Synthesis in MDPs.
Transaction on Automatic Control,
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Ahmadreza Marandi, Marnix Suilen & Ufuk Topcu (2021):
Robust Finite-State Controllers for Uncertain POMDPs,
Available at https://ojs.aaai.org/index.php/AAAI/article/view/17401.
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Ahmadreza Marandi, Marnix Suilen & Ufuk Topcu (2021):
Robust Finite-State Controllers for Uncertain POMDPs.
Available at https://ojs.aaai.org/index.php/AAAI/article/view/17401.
Gregory R Frey, Christopher D Petersen, Frederick A Leve, Ilya V Kolmanovsky & Anouck R Girard (2017):
Constrained Spacecraft Relative Motion Planning Exploiting Periodic Natural Motion Trajectories and Invariance.
Journal of Guidance, Control, and Dynamics 40(12),
Robert Givan, Sonia Leach & Thomas Dean (2000):
Bounded-Parameter Markov Decision Processes.
Artif. Intell. 122(1-2),
Ian Goodfellow, Yoshua Bengio, Aaron Courville & Yoshua Bengio (2016):
Deep learning 1.
Matthew J. Hausknecht & Peter Stone (2015):
Deep Recurrent Q-Learning for Partially Observable MDPs,
Available at http://www.aaai.org/ocs/index.php/FSS/FSS15/paper/view/11673.
Milos Hauskrecht & Hamish Fraser (2000):
Planning treatment of ischemic heart disease with partially observable Markov decision processes.
Artificial Intelligence in Medicine 18(3),
Nicolas Heess, Gregory Wayne, David Silver, Timothy Lillicrap, Tom Erez & Yuval Tassa (2015):
Learning continuous control policies by stochastic value gradients.
Kerianne L Hobbs & Eric M Feron (2020):
A Taxonomy for Aerospace Collision Avoidance with Implications for Automation in Space Traffic Management.
In: AIAA Scitech 2020 Forum,
Nils Jansen, Ralf Wimmer, Erika Ábrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker & Johann Schuster (2014):
Symbolic counterexample generation for large discrete-time Markov chains.
Sci. Comput. Program. 91,
Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen & Bernd Becker (2018):
Finite-State Controllers of POMDPs using Parameter Synthesis.
Available at http://auai.org/uai2018/proceedings/papers/195.pdf.
Leslie Pack Kaelbling, Michael L Littman & Anthony R Cassandra (1998):
Planning and Acting in Partially Observable Stochastic Domains.
Artificial intelligence 101(1-2),
Mykel J Kochenderfer (2015):
Decision Making Under Uncertainty: Theory and Application.
Omid Madani, Steve Hanks & Anne Condon (1999):
On the Undecidability of Probabilistic Planning and Infinite-Horizon Partially Observable Markov Decision Problems.
Marc Mangel & Colin Whitcomb Clark (2019):
Dynamic Modeling in Behavioral Ecology.
Princeton University Press,
Nicolas Meuleau, Kee-Eung Kim, Leslie Pack Kaelbling & Anthony R. Cassandra (1999):
Solving POMDPs by Searching the Space of Finite Policies.
Wim De Mulder, Steven Bethard & Marie-Francine Moens (2015):
A survey on the application of recurrent neural networks to statistical language modeling.
Computer Speech & Language 30(1),
Arnab Nilim & Laurent El Ghaoui (2005):
Robust Control of Markov Decision Processes with Uncertain Transition Matrices.
Operations Research 53(5),
Sylvie C. W. Ong, Shao Wei Png, David Hsu & Wee Sun Lee (2009):
POMDPs for robotic tasks with mixed observability.
In: Robotics: Science and Systems.
The MIT Press,
Amir Pnueli (1977):
The Temporal Logic of Programs.
IEEE Computer Society,
Alex Sherstinsky (2020):
Fundamentals of recurrent neural network (RNN) and long short-term memory (LSTM) network.
Physica D: Nonlinear Phenomena 404,
Matthijs T. J. Spaan & Nikos A. Vlassis (2004):
A Point-based POMDP Algorithm for Robot Planning.
Marnix Suilen, Nils Jansen, Murat Cubuktepe & Ufuk Topcu (2020):
Robust Policy Synthesis for Uncertain POMDPs via Convex Optimization.
Daan Wierstra, Alexander Förster, Jan Peters & Jürgen Schmidhuber (2007):
Solving deep memory POMDPs with recurrent policy gradients.
(Stony Brook University
||The field of formal verification has traditionally looked at
proving properties about finite state machines or software programs. Recent research has also looked at
other classes of systems such as CPS models given with differential equations, or even systems that
include neural networks. We present verification methods and symbolic and numerical challenges and
optimizations that make scalable
analysis increasingly practical.
Reachability methods are useful for proving what future states a system can enter. For
example, given a set of initial states, can any of the states enter an unsafe state?
This invited talk reviews CPS verification methods based on the linear star set data structure.
For this to work efficiently in high dimensions, operations such as affine transformations and intersections must be
In neural networks, formal verification also requires these two key operations, in order to
analyze networks with ReLUs. The open-loop neural network verification problem, show in Figure 1, checks if given
constraints on the inputs, can you prove something about the possible outputs of the network. Doing this efficiently
requires many optimizations that lie at the intersection of symbolic and numeric reasoning. Further, we review
results from VNN-COMP 2021, which completed in July and was the first objective large-scale evaluation of 12
proposed verification tools, done in conjunction with the tool authors.
Figure 1: The open-loop neural network verification problem was
analyzed at VNN-COMP 2021.
(Toyota Research Institute North America, Toyota R & D
||Safety is a critical concern in the development of autonomous mobile system. In this talk, we consider two challenges in this area. First, the verification problem of AMS with machine learning components. Second, the control synthesis problem for start-to-goal requirements while avoiding static and dynamic obstacles. Finally, we provide an overview of the Toyota Human Support Robot as a platform for the development of rigorous methods for the next generation of autonomous mobile systems.
A typical autonomous mobile system (AMS) consists of many subsystems including navigation, localization, perception and motion planning. One or more of these subsystems may utilize machine learning components such as Deep Neural Networks (DNN) to reason over complex behaviors. In this talk, we discuss techniques [4, 6, 7, 1] for the verification of these components and the challenges in this area.
In addition, we provide an overview of the related problem of control synthesis for start-to-goal motion planning with dynamic obstacles and humans in the environment [3
]. This becomes particularly challenging in complex workspaces with narrow corridors and high human activity.
Finally, we provide an an overview of the Human Support Robot (Fig. 1) [5
] as a platform for the development of rigorous methods for the next generation of autonomous mobile systems.