Verse Library

Verse is a Python library for creating, simulating, and verifying scenarios with interacting, decision making agents. The decision logic can be written in an expressive subset of Python. The continuous evolution can be described as a black-box simulation function. The agent can be ported across different maps, which can be defined from scratch or imported from opendrive files. Verse scenarios can be simulated and verified using hybrid reachability analysis. Verse is developed abd maintained by the Reliable Autonomy Research Group at the University of Illinois at Urbana-Champaign.

Installation

The package requires python 3.8+. The package can be installed using pip with all required dependencies

pip install -e .

To update the dependencies in case anything is missing, requirements.txt can be used.

pip install -r requirements.txt

Try

python3 demo/ball/ball_bounces.py

Try other examples in the demo/ folder.

Tutorial

Interactive Jupyter tutorial: tutorial/tutorial.ipynb.

PDF tutorial: tutorial.pdf.

Documentation (in progress): Online.

Read comments in demo/ball/ball_bounces.py and other examples in the demo folder to learn how to create new agents and scenarios.

Using NeuReach with Verse

Verse allows users to plug-in different backend tools for computing reachable sets, specifically, the continuous-post operator. By default, Verse supports DryVR and NeuReach. For NeuReach, additional dependencies can be downloaded:

git submodule init
git submodule update

Library structure

The source code of the package is contained in the verse folder, which contains the following sub-directories.

• verse Building blocks for creating and analyzing scenarios.

  • verse/scenario Scenario base class. A scenario is constructed by several agents with continuous dynamics and controller, a map and a sensor defining how different agents interact with each other.
  • verse/agents Agent base class in the scenario.
  • verse/map Map base class and corresponding utilities in the scenario.
  • verse/code_parser Verse parser for converting the agent's decision logic (transitions) to ASTs.
  • verse/automaton Implements construction of hybrid automaton
  • verse/analysis Simulator and Verifier and related utilities for analysis of the scenario
  • verse/dryvr dryvr for computing reachable sets

• example contains example map, sensor and agents that we provided

• plotter contains code for visualizing the computed results

Contributors

• Katherine Braught
• Yangge Li
• Sayan Mitra
• Keyi Shen
• Haoqing Zhu
• Daniel Zhuang

In order to contribute to this repository, you should run the following commands:

pip install -r requirements-dev.txt
pre-commit install

Related Publications

Verse: A Python library for reasoning about multi-agent hybrid system scenarios Yangge Li, Haoqing Zhu, Katherine Braught, Keyi Shen, Sayan Mitra In the proceedings Computer Aided Verification (CAV), LNCS vol 13964, pages 351–364, 2023.

Verification of L1 Adaptive Control using Verse Library: A Case Study of Quadrotors Lin Song, Yangge Li, Sheng Cheng, Pan Zhao, Sayan Mitra, Naira Hovakimyan In the Work in Progress Session of International Conference on Cyber-Physical Systems (WiP-ICCPS), San Antonio, Tx, 2023.

Parallel and incremental verification of hybrid automata with Ray and Verse Haoqing Zhu, Yangge Li, Keyi Shen, and Sayan Mitra. In the proceedings of 21st Intl. Symposium on Automated Technologies for Verification and Analysis (ATVA), 2023.

Parallelization and incremental algorithms in the verse hybrid system verification library Haoqing Zhu, Masters thesis, University of Illinois at Urbana-Champaign, May 2023.