EPTCS 361
Proceedings The 7th International Workshop on
SymbolicNumeric Methods for Reasoning about CPS and IoT
Online, 23rd August 2021
Edited by: Anne Remke and Dung Hoang Tran
Welcome to the proceedings of the 7th International Workshop on SymbolicNumeric 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 COVID19 pandemic, the whole event took place online. SNR focuses on the combination of symbolic and numeric methods for reasoning about CyberPhysical 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 (Cochair, University of NebraskaLincoln, USA)
 Anne Remke (Cochair, 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 COVID19 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 longrange communication channels with a spacecraft orbiting the earth [15], or the expected responses of human operators [27]. Moreover, sensor limitations may lead to imperfect information of the current state of the system. Yet, autonomous systems often operate in safetycritical 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 [34].
Epistemic POMDPs. The standard models to reason about decisionmaking under uncertainty and imperfect information in artificial intelligence are partially observable Markov decision processes [26] (POMDPs). With a wide range of POMDP applications, such as robotics [33, 36], humanitarian relief aid [5], treatment of heart disease [21], ecology [12, 29], and many more [11]; scalable approaches to verifiable safety have the potential to render decisionmaking 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,
32]. 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 [27]. 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 [28].
(a) Memoryless policy.

(b) Fivememorystate 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,
3] or as control policies [
20,
22]. Yet, RNNs are complex structures that capture nonlinear inputoutput relations [
31], and providing verifiable guarantees on safety is hard [
35,
19].
In this talk we present our approaches to compute socalled
robust finite state controllers (FSCs) [
30,
1] 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 stateoftheart. We show the applicability of the approaches using two case studies, namely aircraft collision avoidance [
27] and spacecraft motion planning [
17,
23]. 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.
Acknowledgements
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 coauthors for the extremely fruitful collaboration.
References

Christopher Amato, Daniel S Bernstein & Shlomo Zilberstein (2010):
Optimizing Fixedsize Stochastic Controllers for POMDPs and Decentralized POMDPs.
AAMAS 21(3),
pp. 293–320,
doi:10.1007/s104580099103z.

Christel Baier & JoostPieter Katoen (2008):
Principles of Model Checking.
MIT Press.

Bram Bakker (2001):
Reinforcement Learning with Long ShortTerm Memory.
In: NIPS.
MIT Press,
pp. 1475–1482,
doi:10.5555/2980539.2980731.
Available at https://proceedings.neurips.cc/paper/2001/hash/a38b16173474ba8b1a95bcbc30d3b8a5Abstract.html.

Stephen Boyd & Lieven Vandenberghe (2004):
Convex optimization.
Cambridge university press,
doi:10.1017/CBO9780511804441.

Raissa Zurli Bittencourt Bravo, Adriana Leiras & Fernando Luiz Cyrino Oliveira (2019):
The Use of UAV s in Humanitarian Relief: An Application of POMDPBased Methodology for Finding Victims.
Production and Operations Management 28(2),
pp. 421–440,
doi:10.1111/poms.12930.

Brendan Burns & Oliver Brock (2007):
SamplingBased Motion Planning with Sensing Uncertainty.
In: ICRA.
IEEE,
pp. 3313–3318,
doi:10.1109/ROBOT.2007.363984.

Steven Carr, Nils Jansen & Ufuk Topcu (2020):
Verifiable RNNBased Policies for POMDPs Under Temporal Logic Constraints.
In: IJCAI.
ijcai.org,
pp. 4121–4127,
doi:10.24963/ijcai.2020/570.

Steven Carr, Nils Jansen & Ufuk Topcu (2021):
TaskAware Verifiable RNNBased Policies for Partially Observable Markov Decision Processes.
Journal of Artificial Intelligence Research 72,
pp. 819–847,
doi:10.1613/jair.1.12963.

Steven Carr, Nils Jansen, Ralf Wimmer, Jie Fu & Ufuk Topcu (2018):
HumanintheLoop Synthesis for Partially Observable Markov Decision Processes.
In: ACC.
IEEE,
pp. 762–769,
doi:10.23919/ACC.2018.8431911.

Steven Carr, Nils Jansen, Ralf Wimmer, Alexandru Constantin Serban, Bernd Becker & Ufuk Topcu (2019):
CounterexampleGuided Strategy Improvement for POMDPs Using Recurrent Neural Networks.
In: IJCAI.
ijcai.org,
pp. 5532–5539,
doi:10.24963/ijcai.2019/768.

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 McDonaldMadden, 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),
pp. 13936–13940,
doi:10.1073/pnas.0805265105.

Edmund M Clarke, Thomas A Henzinger, Helmut Veith & Roderick Bloem (2018):
Handbook of model checking 10.
Springer,
doi:10.1007/9783319105758.

Murat Cubuktepe, Nils Jansen, Sebastian Junges, JoostPieter Katoen & Ufuk Topcu (2021):
Convex Optimization for Parameter Synthesis in MDPs.
Transaction on Automatic Control,
pp. 11,
doi:10.1109/TAC.2021.3133265.

Murat Cubuktepe, Nils Jansen, Sebastian Junges, Ahmadreza Marandi, Marnix Suilen & Ufuk Topcu (2021):
Robust FiniteState Controllers for Uncertain POMDPs,
pp. 11792–11800.
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 FiniteState Controllers for Uncertain POMDPs.
In: AAAI.
AAAI Press,
pp. 11792–11800.
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),
pp. 3100–3115,
doi:10.2514/1.G002914.

Robert Givan, Sonia Leach & Thomas Dean (2000):
BoundedParameter Markov Decision Processes.
Artif. Intell. 122(12),
pp. 71–109,
doi:10.1109/CDC40024.2019.9029460.

Ian Goodfellow, Yoshua Bengio, Aaron Courville & Yoshua Bengio (2016):
Deep learning 1.
MIT Press.

Matthew J. Hausknecht & Peter Stone (2015):
Deep Recurrent QLearning for Partially Observable MDPs,
pp. 29–37.
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),
pp. 221–244,
doi:10.1016/S09333657(99)000421.

Nicolas Heess, Gregory Wayne, David Silver, Timothy Lillicrap, Tom Erez & Yuval Tassa (2015):
Learning continuous control policies by stochastic value gradients.
In: NIPS,
pp. 2944–2952.

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,
pp. 0877,
doi:10.2514/6.20200877.

Nils Jansen, Ralf Wimmer, Erika Ábrahám, Barna Zajzon, JoostPieter Katoen, Bernd Becker & Johann Schuster (2014):
Symbolic counterexample generation for large discretetime Markov chains.
Sci. Comput. Program. 91,
pp. 90–114,
doi:10.1016/j.scico.2014.02.001.

Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, JoostPieter Katoen & Bernd Becker (2018):
FiniteState Controllers of POMDPs using Parameter Synthesis.
In: UAI,
pp. 519–529.
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(12),
pp. 99–134,
doi:10.1016/S00043702(98)00023X.

Mykel J Kochenderfer (2015):
Decision Making Under Uncertainty: Theory and Application.
MIT press,
doi:10.7551/mitpress/10187.001.0001.

Omid Madani, Steve Hanks & Anne Condon (1999):
On the Undecidability of Probabilistic Planning and InfiniteHorizon Partially Observable Markov Decision Problems.
In: AAAI.
AAAI Press,
pp. 541–548.

Marc Mangel & Colin Whitcomb Clark (2019):
Dynamic Modeling in Behavioral Ecology.
Princeton University Press,
doi:10.2307/j.ctvs32s5v.

Nicolas Meuleau, KeeEung Kim, Leslie Pack Kaelbling & Anthony R. Cassandra (1999):
Solving POMDPs by Searching the Space of Finite Policies.
In: UAI,
pp. 417–426,
doi:10.5555/2073796.2073844.

Wim De Mulder, Steven Bethard & MarieFrancine Moens (2015):
A survey on the application of recurrent neural networks to statistical language modeling.
Computer Speech & Language 30(1),
pp. 61–98,
doi:10.1016/j.csl.2014.09.005.

Arnab Nilim & Laurent El Ghaoui (2005):
Robust Control of Markov Decision Processes with Uncertain Transition Matrices.
Operations Research 53(5),
pp. 780–798,
doi:10.1287/opre.1050.0216.

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,
doi:10.15607/RSS.2009.V.026.

Amir Pnueli (1977):
The Temporal Logic of Programs.
In: FOCS.
IEEE Computer Society,
pp. 46–57,
doi:10.1109/SFCS.1977.32.

Alex Sherstinsky (2020):
Fundamentals of recurrent neural network (RNN) and long shortterm memory (LSTM) network.
Physica D: Nonlinear Phenomena 404,
pp. 132306,
doi:10.1016/j.physd.2019.132306.

Matthijs T. J. Spaan & Nikos A. Vlassis (2004):
A Pointbased POMDP Algorithm for Robot Planning.
In: ICRA.
IEEE,
pp. 2399–2404,
doi:10.1109/ROBOT.2004.1307420.

Marnix Suilen, Nils Jansen, Murat Cubuktepe & Ufuk Topcu (2020):
Robust Policy Synthesis for Uncertain POMDPs via Convex Optimization.
In: IJCAI.
ijcai.org,
pp. 4113–4120,
doi:10.5555/3491440.3492009.

Daan Wierstra, Alexander Förster, Jan Peters & Jürgen Schmidhuber (2007):
Solving deep memory POMDPs with recurrent policy gradients.
In: ICANN.
Springer,
pp. 697–706,
doi:10.1007/9783540746904_71.
Stanley Bak (
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. 

1 Overview
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
supported.
In neural networks, formal verification also requires these two key operations, in order to
analyze networks with ReLUs. The openloop 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 VNNCOMP 2021, which completed in July and was the first objective largescale evaluation of 12
proposed verification tools, done in conjunction with the tool authors.
Figure 1: The openloop neural network verification problem was
analyzed at VNNCOMP 2021.
Bardh Hoxha (
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 starttogoal 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. 

1 Introduction
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 starttogoal motion planning with dynamic obstacles and humans in the environment [
3,
2]. 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.