Published: 14th July 2022
DOI: 10.4204/EPTCS.361
ISSN: 2075-2180

EPTCS 361

Proceedings The 7th International Workshop on
Symbolic-Numeric Methods for Reasoning about CPS and IoT
Online, 23rd August 2021

Edited by: Anne Remke and Dung Hoang Tran
Preface
Dung Tran and Anne Remke
Invited Presentation: Safe Planning under Epistemic Uncertainty and Partial Information
Nils Jansen		1
Invited Presentation: Symbolic and Numeric Challenges in Neural Network Verification Methods
Stanley Bak		5
Invited Presentation: Verification and Control for Autonomous Mobile Systems
Bardh Hoxha		7
Model Checking for Rectangular Hybrid Systems: A Quantified Encoding Approach
Luan V. Nguyen, Wesam Haddad and Taylor T. Johnson		9
Time-Staging Enhancement of Hybrid System Falsification
Gidon Ernst, Ichiro Hasuo, Zhenya Zhang and Sean Sedwards		25
Verification of Sigmoidal Artificial Neural Networks using iSAT
Dominik Grundt, Sorin Liviu Jurj, Willem Hagemann, Paul Kröger and Martin Fränzle		45
Robot Swarms as Hybrid Systems: Modelling and Verification
Stefan Schupp, Francesco Leofante, Leander Behr, Erika Ábrahám and Armando Taccella		61
Work In Progress: Safety and Robustness Verification of Autoencoder-Based Regression Models using the NNV Tool
Neelanjana Pal and Taylor T Johnson		79

Preface


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:

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:

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)

Safe Planning under Epistemic Uncertainty and Partial Information

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 [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 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 [34].

Epistemic POMDPs. The standard models to reason about decision-making 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 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, 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) 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, 3] or as control policies [20, 22]. Yet, RNNs are complex structures that capture non-linear input-output relations [31], and providing verifiable guarantees on safety is hard [35, 19].

In this talk we present our approaches to compute so-called 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 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, 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 co-authors for the extremely fruitful collaboration.

References

  1. Christopher Amato, Daniel S Bernstein & Shlomo Zilberstein (2010): Optimizing Fixed-size Stochastic Controllers for POMDPs and Decentralized POMDPs. AAMAS 21(3), pp. 293–320, doi:10.1007/s10458-009-9103-z.
  2. Christel Baier & Joost-Pieter Katoen (2008): Principles of Model Checking. MIT Press.
  3. Bram Bakker (2001): Reinforcement Learning with Long Short-Term Memory. In: NIPS. MIT Press, pp. 1475–1482, doi:10.5555/2980539.2980731. Available at https://proceedings.neurips.cc/paper/2001/hash/a38b16173474ba8b1a95bcbc30d3b8a5-Abstract.html.
  4. Stephen Boyd & Lieven Vandenberghe (2004): Convex optimization. Cambridge university press, doi:10.1017/CBO9780511804441.
  5. 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), pp. 421–440, doi:10.1111/poms.12930.
  6. Brendan Burns & Oliver Brock (2007): Sampling-Based Motion Planning with Sensing Uncertainty. In: ICRA. IEEE, pp. 3313–3318, doi:10.1109/ROBOT.2007.363984.
  7. Steven Carr, Nils Jansen & Ufuk Topcu (2020): Verifiable RNN-Based Policies for POMDPs Under Temporal Logic Constraints. In: IJCAI. ijcai.org, pp. 4121–4127, doi:10.24963/ijcai.2020/570.
  8. 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, pp. 819–847, doi:10.1613/jair.1.12963.
  9. Steven Carr, Nils Jansen, Ralf Wimmer, Jie Fu & Ufuk Topcu (2018): Human-in-the-Loop Synthesis for Partially Observable Markov Decision Processes. In: ACC. IEEE, pp. 762–769, doi:10.23919/ACC.2018.8431911.
  10. Steven Carr, Nils Jansen, Ralf Wimmer, Alexandru Constantin Serban, Bernd Becker & Ufuk Topcu (2019): Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks. In: IJCAI. ijcai.org, pp. 5532–5539, doi:10.24963/ijcai.2019/768.
  11. 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.
  12. 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), pp. 13936–13940, doi:10.1073/pnas.0805265105.
  13. Edmund M Clarke, Thomas A Henzinger, Helmut Veith & Roderick Bloem (2018): Handbook of model checking 10. Springer, doi:10.1007/978-3-319-10575-8.
  14. Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen & Ufuk Topcu (2021): Convex Optimization for Parameter Synthesis in MDPs. Transaction on Automatic Control, pp. 1-1, doi:10.1109/TAC.2021.3133265.
  15. Murat Cubuktepe, Nils Jansen, Sebastian Junges, Ahmadreza Marandi, Marnix Suilen & Ufuk Topcu (2021): Robust Finite-State Controllers for Uncertain POMDPs, pp. 11792–11800. Available at https://ojs.aaai.org/index.php/AAAI/article/view/17401.
  16. Murat Cubuktepe, Nils Jansen, Sebastian Junges, Ahmadreza Marandi, Marnix Suilen & Ufuk Topcu (2021): Robust Finite-State Controllers for Uncertain POMDPs. In: AAAI. AAAI Press, pp. 11792–11800. Available at https://ojs.aaai.org/index.php/AAAI/article/view/17401.
  17. 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.
  18. Robert Givan, Sonia Leach & Thomas Dean (2000): Bounded-Parameter Markov Decision Processes. Artif. Intell. 122(1-2), pp. 71–109, doi:10.1109/CDC40024.2019.9029460.
  19. Ian Goodfellow, Yoshua Bengio, Aaron Courville & Yoshua Bengio (2016): Deep learning 1. MIT Press.
  20. Matthew J. Hausknecht & Peter Stone (2015): Deep Recurrent Q-Learning for Partially Observable MDPs, pp. 29–37. Available at http://www.aaai.org/ocs/index.php/FSS/FSS15/paper/view/11673.
  21. 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/S0933-3657(99)00042-1.
  22. 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.
  23. 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.2020-0877.
  24. 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, pp. 90–114, doi:10.1016/j.scico.2014.02.001.
  25. Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen & Bernd Becker (2018): Finite-State Controllers of POMDPs using Parameter Synthesis. In: UAI, pp. 519–529. Available at http://auai.org/uai2018/proceedings/papers/195.pdf.
  26. Leslie Pack Kaelbling, Michael L Littman & Anthony R Cassandra (1998): Planning and Acting in Partially Observable Stochastic Domains. Artificial intelligence 101(1-2), pp. 99–134, doi:10.1016/S0004-3702(98)00023-X.
  27. Mykel J Kochenderfer (2015): Decision Making Under Uncertainty: Theory and Application. MIT press, doi:10.7551/mitpress/10187.001.0001.
  28. Omid Madani, Steve Hanks & Anne Condon (1999): On the Undecidability of Probabilistic Planning and Infinite-Horizon Partially Observable Markov Decision Problems. In: AAAI. AAAI Press, pp. 541–548.
  29. Marc Mangel & Colin Whitcomb Clark (2019): Dynamic Modeling in Behavioral Ecology. Princeton University Press, doi:10.2307/j.ctvs32s5v.
  30. Nicolas Meuleau, Kee-Eung 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.
  31. 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), pp. 61–98, doi:10.1016/j.csl.2014.09.005.
  32. 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.
  33. 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.
  34. Amir Pnueli (1977): The Temporal Logic of Programs. In: FOCS. IEEE Computer Society, pp. 46–57, doi:10.1109/SFCS.1977.32.
  35. Alex Sherstinsky (2020): Fundamentals of recurrent neural network (RNN) and long short-term memory (LSTM) network. Physica D: Nonlinear Phenomena 404, pp. 132306, doi:10.1016/j.physd.2019.132306.
  36. Matthijs T. J. Spaan & Nikos A. Vlassis (2004): A Point-based POMDP Algorithm for Robot Planning. In: ICRA. IEEE, pp. 2399–2404, doi:10.1109/ROBOT.2004.1307420.
  37. 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.
  38. 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/978-3-540-74690-4_71.

Symbolic and Numeric Challenges in Neural Network Verification Methods

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 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.

 

 

Verification and Control for Autonomous Mobile Systems

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 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.  

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 start-to-goal 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.

 

Figure 1: Left: Human Support Robot; Right: Human support robot operating alongside humans.

References

  1. Joseph Cralley, Ourania Spantidi, Bardh Hoxha & Georgios Fainekos (2020): TLTk: A Toolbox for Parallel Robustness Computation of Temporal Logic Specifications. In: Jyotirmoy Deshmukh & Dejan Nickovic: Runtime Verification - 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6-9, 2020, Proceedings, Lecture Notes in Computer Science 12399. Springer, pp. 404–416, doi:10.1007/978-3-030-60508-7_22.
  2. Keyvan Majd, Shakiba Yaghoubi, Tomoya Yamaguchi, Bardh Hoxha, Danil V. Prokhorov & Georgios Fainekos (2021): Safe Navigation in Human Occupied Environments Using Sampling and Control Barrier Functions. In: IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2021, Prague, Czech Republic, September 27 - Oct. 1, 2021. IEEE, pp. 5794–5800, doi:10.1109/IROS51168.2021.9636406.
  3. Shakiba Yaghoubi, Keyvan Majd, Georgios Fainekos, Tomoya Yamaguchi, Danil Prokhorov & Bardh Hoxha (2020): Risk-bounded control using stochastic barrier functions. IEEE Control Systems Letters 5(5), pp. 1831–1836, doi:10.1109/LCSYS.2020.3043287.
  4. Tomoya Yamaguchi, Bardh Hoxha, Danil Prokhorov & Jyotirmoy V Deshmukh (2020): Specification-guided software fault localization for autonomous mobile systems. In: 2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). IEEE, pp. 1–12, doi:10.1109/MEMOCODE51338.2020.9315067.
  5. Takashi Yamamoto, Koji Terada, Akiyoshi Ochiai, Fuminori Saito, Yoshiaki Asahara & Kazuto Murase (2019): Development of Human Support Robot as the research platform of a domestic mobile manipulator. ROBOMECH Journal 6(1), pp. 4, doi:10.1186/s40648-019-0132-3.
  6. Xiaodong Yang, Taylor T. Johnson, Hoang-Dung Tran, Tomoya Yamaguchi, Bardh Hoxha & Danil V. Prokhorov (2021): Reachability analysis of deep ReLU neural networks using facet-vertex incidence. In: Sergiy Bogomolov & Raphaël M. Jungers: HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control, Nashville, Tennessee, May 19-21, 2021. ACM, pp. 18:1–18:7, doi:10.1145/3447928.3456650.
  7. Xiaodong Yang, Tomoya Yamaguchi, Hoang-Dung Tran, Bardh Hoxha, Taylor T Johnson & Danil Prokhorov (2021): Reachability Analysis of Convolutional Neural Networks. arXiv preprint arXiv:2106.12074.