Keywords

figure a
figure b

1 Introduction

Automatic verification tools for hybrid systems have been used to analyze linear models with thousands of continuous dimensions [1, 5, 6] and nonlinear models inspired by industrial applications [6, 14]. The state of the art and the challenges are discussed in a recent survey [11]. Despite the potentially large user base, currently this technology is inaccessible without formal methods training. Automatic hybrid verification tools [10, 13, 17, 25, 31] require the input model to be written in a tool-specific language. Tools like C2E2 [15] attempt to translate models from Simulink/Stateflow, but the language-barrier goes down to the underlying math models. The verification algorithms are based on variants of the hybrid automaton [3, 21, 24] which requires the discrete states (or modes) to be spelled out explicitly as a graph, with guards and resets labeling the transitions. We discuss related works in more detail in Sect. 6, including recently developed libraries that address usability barrier [5, 7, 8].

In this paper, we present Verse, a Python library that aims to make hybrid technologies more usable for multi-agent scenarios. The key features implemented are as follows: (1) In Verse, users write scenarios in Python. User-defined functions can be used to create complex agents, invariant requirements can be written as assert statements, and scenarios can be created by instantiating multiple agents, all using the standard Python syntax. Verse parses this scenario and constructs an internal representation of the hybrid automaton for simulation and analysis. (2) Verse introduces an additional structure, called map, for defining the modes and the transitions of a hybrid system. Map contains tracks that can capture geometric objects (e.g., lanes or waypoints) that make it possible to create new scenarios just by instantiating agents on new maps. With track modes, users do not have to explicitly write different modes for a vehicle following different waypoint segments. Finally, (3) Verse comes with functions for simulation and safety verification via reachability analysis. Developers can implement new functions, plug-in existing tools, or implement advanced algorithms, e.g., for incremental verification. In this tool paper, we illustrate use cases with heterogeneous agents and different scenario setups, the flexibility of plugging in different reachability algorithms and the ability to develop more advanced algorithms (Sect. 5). Verse is available at https://github.com/AutoVerse-ai/Verse-library.

2 Overview of Verse

We will highlight the key features of Verse with an example. Consider two drones flying along three parallel \(\infty \)-shaped tracks that are vertically separated in space (shown by black lines in Fig. 1). Each drone has a simple collision avoidance logic: if it gets too close to another drone on the same track, then it switches to either the track above or the one below. A drone on T1 has both choices. Verse enables creation, simulation, and verification of such scenarios using Python, and provides a collection of powerful functions for building new analysis algorithms.

Fig. 1.
figure 1

Left: A 3-d \(\infty \)-shaped map with example track mode labels. Center: Simulation of a red drone nearing the blue drone on T1 and nondeterministically moving to T0 or T2. Both branches are computed by Verse ’s simulate function. Right: Computed reachable sets of the two drones cover more possibilities: either drones can switch tracks when they get close. All four branches are explored by Verse. The branch for blue drone moving downwards violates safety as it may collide with the red drone following T1.

Full size image

Creating Scenarios. Agents like the drones in this example are described by a simulator and a decision logic in an expressive subset of Python (see code in Fig. 2 and [26] for more details). The decision logic for an ego agent takes as input its current state and the (observable) states of the other agents, and updates the discrete state or the mode of the ego agent. For example, in lines 41–43 of Fig. 2 an agent updates its mode to begin a track change if there is any agent near it. It may also update the continuous state of the ego agent. The mode of an agent, as we shall see later in Sect. 3, has two parts—a tactical mode corresponding to agent’s decision or discrete state, and a track mode that is determined by the map. Using the any and all functions, the agent’s decision logic can quantify over other agents in the scene. User defined functions are also allowed (is_close, Fig. 2 line 41). Verse will parse this decision logic to create an internal representation of the transition graph of the hybrid model with guards and resets. The simulator can be written in any language and is treated as a black-boxFootnote 1. For the examples discussed in this paper, the simulators are also written in Python. Safety requirements can be specified using assert statements (see Fig. 5).

Fig. 2.
figure 2

Decision Logic Code Snippet from drone\(\_\)controller.py.

Full size image

Maps and Sensors. The map of a scenario specifies the tracks that the agents can follow. While a map may have infinitely many tracks, they fall in a finite number of track modes. For example, in this \(\infty \)-shaped map, each layer is assigned to a track mode (T0-2) and all the tracks between each pair of layers are also assigned to a track mode (M10, M01 etc.). When an agent makes a decision and changes its tactical mode, the map object determines the new track mode for the agent. The map abstraction makes scenarios succinct and enables portability of agents across different maps. Besides creating from scratch, Verse provides functions for generating map objects from OpenDRIVE [4] files.

The sensor function defines which variables from an agent are visible to other agents. The default sensor function allows all agents to see all variables; we discuss how the sensor function can be modified to include bounded noise in Sect. 5. A map, a sensor and a collection of (compatible) agents together define a scenario object (Fig. 3). In the first few lines, the drone agents are created, initialized, and added to the scenario object. A scenario can have heterogeneous agents with different decision logics.

Fig. 3.
figure 3

Scenario specification snippet.

Full size image

Simulation and Reachability. Once a scenario is defined, Verse ’s simulate function can generate simulation(s) of the system, which can be stored and plotted. As shown in Fig. 1(Center), a simulation from a single initial state explores all possible branches that can be generated by the decision logics of the interacting agents, upto a specified time horizon. Verse verifies the safety assertions of a scenario by computing the over-approximations of the reachable sets for each agent, and checking these against the predicates defined by the assertions. Figure 1(Right) visualizes the result of such a computation performed using the verify function. In this example, the safety condition is violated when the blue drone moves downward to avoid the red drone. The other branches of the scenario are proved to be safe. The simulate and verify functions save a copy of the resulting execution tree, which can be loaded and traversed to analyze the sequences modes and states that leads to safety violations. Verse makes it convenient to plug in different reachability subroutines. It also provides powerful functions to implement advanced verification algorithms, such as incremental verification.

3 Scenarios in Verse

A scenario in Verse is specified by a map, a collection of agents in that map, and a sensor function that defines the part of each agent visible to other agents. We describe these components below, and in Sect. 4, we will discuss how they formally define a hybrid system.

Tracks, Track Modes, and Maps. A workspace \({W}\) is an Euclidean space in which the agents reside (For example, a compact subset of \({\mathbb {R}}^2\) or \({\mathbb {R}}^3\)). An agent’s continuous dynamics makes it roughly follow certain continuous curves in \({W}\), called tracks, and occasionally the agent’s decision logic changes the track. Formally, a track is simply a continuous function \({\omega }: [0,1]\rightarrow {W}\), but not all such functions are valid tracks. A map \(\mathcal {M}\) defines the set of tracks \({\varOmega } _\mathcal {M}\) it permits. In a highway map, some tracks will be aligned along the lanes while others will correspond to merges and exits.

We assume that an agent’s decision logic does not depend on exactly which of the infinitely many tracks it is following, but instead, it depends only on which type of track it is following or the track mode. In the example in Sect. 2, the track modes are T0, T1, M01, etc. Every (blue) track for transitioning from point on T0 to the corresponding point on T1 has track mode M01. A map has a finite set of track modes \({L} _\mathcal {M}\) and a labeling function \({V}_\mathcal {M}: {\varOmega } _\mathcal {M}\rightarrow {L} _\mathcal {M}\) that maps the track to a track mode. It also has a mapping \({g} _\mathcal {M}: {W}\times {L} _\mathcal {M}\rightarrow {\varOmega } _\mathcal {M}\) that maps a track mode and a specific position in the workspace to a specific track.

Finally, a Verse agent’s decision logic can change its internal mode or tactical mode \({P} \) (E.g., Normal to MoveUp). When an agent changes its tactical mode, it may also update the track it is following and this is encoded in the track graph function: \({T_g} _\mathcal {M}: {L} _\mathcal {M}\times {P} \times {P} \rightarrow {L} _\mathcal {M}\) which takes the current track mode, the current and the next tactical mode, and generates the new track mode the agent should follow. For example, when the tactical mode of a drone changes from Normal to MoveUP while it is on T1, this map function \({T_g} _\mathcal {M}(\texttt {T1}, \texttt {Normal}, \texttt {MoveUp}) = \texttt {M10}\) informs that the agent should follow a track with mode \(\texttt {M10}\). These sets and functions together define a Verse map object \(\mathcal {M}= \langle {L} _\mathcal {M}, {V}_\mathcal {M},{g} _\mathcal {M}, {T_g} _\mathcal {M}\rangle \). We will drop the subscript \(\mathcal {M}\) when the map being used is clear from context.

Agents. A Verse agent is defined by modes and continuous state variables, a decision logic that defines (possibly nondeterministic) discrete transitions, and a flow function that defines continuous evolution. An agent \(\mathcal {A}\) is compatible with a map \(\mathcal {M}\) if the agent’s tactical modes \({P} \) are a subset of the allowed input tactical modes for \({T_g} \). This makes it possible to instantiate the same agent on different compatible maps. The mode space for an agent instantiated on map \(\mathcal {M}\) is the set \({D}= {L} \times {P} \), where \({L} \) is the set of track modes in \(\mathcal {M}\) and \({P} \) is the set of tactical modes of the agent. The continuous state space is \({X}= {W}\times {Z}\), where \({W}\) is the workspace (of \(\mathcal {M}\)) and \({Z}\) is the space of other continuous state variables. The (full) state space is the Cartesian product \({Y}= {X}\times {D}\). In the two-drone example in Sect. 2, the continuous states variables are the positions and velocities along the three axes of the workspace. The modes are \(\langle \texttt {Normal},\texttt {T1} \rangle \), \(\langle \texttt {MoveUp},\texttt {M10}\rangle \), etc.

An agent \(\mathcal {A}\) in map \(\mathcal {M}\) with \(k-1\) other agents is defined by a tuple \(\mathcal {A}= \langle {Y}, {Y}^0, {G}, {R}, {F}\rangle \), where \({Y}\) is the state space, \({Y}^0 \subseteq {Y}\) is the set of initial states. The guard \({G} \) and reset \({R} \) functions jointly define the discrete transitions. For a pair of modes \({d}, {d}' \in {D},\) \({G} ({d},{d}') \subseteq {X}^k\) defines the condition under which a transition from \({d}\) to \({d}'\) is enabled. The \({R} ({d}, {d}'):{X}^k \rightarrow {X}\) function specifies how the continuous states of the agent are updated when the mode switch happens. Both of these functions take as input the sensed continuous states of all the other \(k-1\) agents in the scenario. The \({G} \) and the \({R} \) functions are not defined separately, but are extracted by the Verse parser from a block of structured Python code as shown in Fig. 2. The discrete states in if conditions and assignments define the source and destination of discrete transitions. if conditions involving continuous states define guards for the transitions and assignments of continuous states define resets. Expressions with \(\texttt {any}\) and \(\texttt {all}\) functions are unrolled to disjunctions and conjunctions according to the number of agents k.

For example in Fig. 2, Lines 47–50 define transitions \(\langle \texttt {MoveUp},\texttt {M10}\rangle \) to \(\langle \texttt {Normal},\texttt {T0}\rangle \) and \(\langle \texttt {MoveUp},\texttt {M21}\rangle \) to \(\langle \texttt {Normal},\texttt {T1}\rangle \). The change of track mode is given by the \({T_g} \) function. The guard for this transition comes from the if condition at Line 48, \({G} (\langle \texttt {MoveUp},\texttt {M10}\rangle , \langle \texttt {Normal},\texttt {T0}\rangle ) = \{{x}\mid -1<\texttt {T0}.pz-{x}.pz<1\}\) for \({x}\in {X}\) given by user defined in_interval function. Here continuous states remain unchanged after transition.

The final component of the agent is the flow function \({F}: {X}\times {D}\times {\mathbb {R}}^{\ge 0} \rightarrow {X}\) which defines the continuous time evolution of the continuous state. For any initial condition \(\langle {x}^0,{d}^0\rangle \in Y\), \(F({x}^0,{d}^0)(\cdot )\) gives the continuous state of the agent as a function of time. In this paper, we use F as a black-box function (see Footnote 1).

Sensors and Scenarios. For a scenario with k agents, a sensor function \(\mathcal {S}:{Y}^k \rightarrow {Y}^{k}\) defines the continuous observables as a function of the continuous state. For simplifying exposition, in this paper we assume that observables have the same type as the continuous state Y, and that each agent i is observed by all other agents identically. This simple, overtly transparent sensor model, still allows us to write realistic agents that only use information about nearby agents. In a highway scenario, the observable part of agent j to another agent i may be the relative distance \(y_{j} = x_j - x_i\), and vice versa, which can be computed as a function of the continuous state variables \(x_j\) and \(x_i\). A different sensor function which gives nondeterministic noisy observations, appears in Sect. 5.

A Verse scenario \({SC}\) is defined by (a) a map \(\mathcal {M}\), (b) a collection of k agent instances \(\{\mathcal {A}_1 ... \mathcal {A}_k\}\) that are compatible with \(\mathcal {M}\), and (c) a sensor \(\mathcal {S}\) for the k agents. Since all the agents are instantiated on the same compatible map \(\mathcal {M}\), they share the same workspace. Currently, we require agents to have identical state spaces, i.e., \({Y}_i = {Y}_j\), but they can have different decision logics and different continuous dynamics.

4 Verse Scenario to Hybrid Verification

In this section, we define the underlying hybrid system \({H}({SC})\), that a Verse scenario \({SC}\) specifies. The verification questions that Verse is equipped to answer are stated in terms of the behaviors or executions of \({H}({SC})\). Verse ’s notion of a hybrid automaton is close to that in Definition 5 of [14]. The only uncommon aspect in [14] is that the continuous flows may be defined by a black-box simulator functions, instead of white-box analytical models (see Footnote 1).

Given a scenario with k agents \({SC}= \langle \mathcal {M}, \{\mathcal {A}_1,...\mathcal {A}_k\}, \mathcal {S}, {P} \rangle \), the corresponding hybrid automaton \({H}({SC}) = \langle {\textbf {X}}, {\textbf {X}}^0, {\textbf {D}}, {\textbf {D}} ^0, {\textbf {G}}, {\textbf {R}}, {\textbf {TL}}\rangle \), where

  1. 1.

    \({\textbf {X}}:= \prod _i {X}_i\) is the continuous state space. An element \({\textbf {x}}\in {\textbf {X}}\) is called a state. \({\textbf {X}}^0 := \prod _i {X}_i^0 \subseteq {\textbf {X}}\) is the set of initial continuous states.

  2. 2.

    \({\textbf {D}}:= \prod _i {D}_i\) is the mode space. An element \({\textbf {d}} \in {\textbf {D}} \) is called a mode. \({\textbf {D}} ^{0} := \prod _i {D}_i^0 \subseteq {\textbf {D}} \) is the finite set of initial modes.

  3. 3.

    For a mode pair \({\textbf {d}}, {\textbf {d}} ' \in {\textbf {D}} \), \({\textbf {G}}({\textbf {d}}, {\textbf {d}} ') \subseteq {\textbf {X}}\) defines the continuous states from which a transition from \({\textbf {d}} \) to \( {\textbf {d}} '\) is enabled. A state \({\textbf {x}}\in {\textbf {G}}({\textbf {d}}, {\textbf {d}} ')\) iff there exists an agent \(i \in \{1,...,k\}\), such that \({\textbf {x}}_i \in {G} _i({\textbf {d}} _i, {\textbf {d}} _i')\) and \({\textbf {d}} _j={\textbf {d}} _j'\) for \(j\ne i\).

  4. 4.

    For a mode pair \({\textbf {d}}, {\textbf {d}} ' \in {\textbf {D}} \), \({\textbf {R}}({\textbf {d}}, {\textbf {d}} '):{\textbf {X}}\rightarrow {\textbf {X}}\) defines the change of continuous states after a transition from \({\textbf {d}} \) to \({\textbf {d}} '\). For a continuous state \({\textbf {x}}\in {\textbf {X}}\), \({\textbf {R}}({\textbf {d}}, {\textbf {d}} ')({\textbf {x}}) = {R} _i({\textbf {d}} _i, {\textbf {d}} _i')({\textbf {x}}) \text { if } {\textbf {x}}\in {G} _i({\textbf {d}} _i, {\textbf {d}} _i')\), otherwise \(= {\textbf {x}}_i\).

  5. 5.

    \({\textbf {TL}}\) is a set of pairs \(\langle \xi , {\textbf {d}} \rangle \), where the trajectory \(\xi :[0,T] \rightarrow {\textbf {X}}\) describes the evolution of continuous states in mode \({\textbf {d}} \in {\textbf {D}} \). Given \({\textbf {d}} \in {\textbf {D}}, {\textbf {x}}^0\in {\textbf {X}}\), \(\xi \) should satisfy \(\forall t\in {\mathbb {R}}^{\ge 0}, \xi _i(t) = F_i({\textbf {x}}^0_i, {\textbf {d}} _i)(t)\).

We denote by \(\xi .fstate\), \(\xi .lstate\), and \(\xi .ltime\) the initial state \(\xi (0)\), the last state \(\xi (T)\), and \(\xi .ltime = T\). For a sampling parameter \(\delta >0\) and a length m, a \(\delta \)-execution of a hybrid automaton \({H}= {H}({SC})\) is a sequence of m labeled trajectories \({\alpha }:= \langle \xi ^0, {\textbf {d}} ^0\rangle ,...,\langle \xi ^{m-1}, {\textbf {d}} ^{m-1}\rangle \), such that (1) \(\xi ^0.fstate \in {\textbf {X}}^0, {\textbf {d}} ^0 \in {\textbf {D}} ^0\), (2) For each \(i \in \{1,...,m-1\}\), \(\xi _i.lstate\in {\textbf {G}}({\textbf {d}} ^i, {\textbf {d}} ^{i+1})\) and \(\xi ^{i+1}.fstate = {\textbf {R}}({\textbf {d}} ^i, {\textbf {d}} ^{i+1})(\xi ^i.lstate)\), and (3) For each \(i \in \{1,...,m-1\}\), \(\xi ^i.ltime = \delta \) for \(i\ne m-1\) and \(\xi ^i.ltime \le \delta \) for \(i=m-1\).

We define first and last state of an execution \({\alpha }= \langle \xi ^0, {\textbf {d}} ^0\rangle ,...,\langle \xi ^{m-1}, {\textbf {d}} ^{m-1}\rangle \) as \({\alpha }.fstate = \xi ^0.fstate\), \({\alpha }.lstate=\xi ^{m-1}.lstate\) and the first and last mode as \({\alpha }.fmode = {\textbf {d}} ^0\) and \({\alpha }.lmode = {\textbf {d}} ^{m-1}\). The set of reachable states is defined by \({Reach_{{H}_{}}} := \{{\alpha }.lstate \mid {\alpha }\text { is an execution of }{H}\}\). In addition, we denote the reachable states in a specific mode \({\textbf {d}} \in {\textbf {V}}\) as \({Reach_{{H}_{}}} ({\textbf {d}})\) and \({Reach_{{H}_{}}} (T)\) to be the set of reachable states at time T. Similarly, denoting the unsafe states for mode \({\textbf {d}} \) as \({\textbf {U}}({\textbf {d}})\), the safety verification problem for \({H}\) can be solved by checking whether \(\forall {\textbf {d}} \in {\textbf {D}} \), \({Reach_{{H}_{}}} ({\textbf {d}}) \cap {\textbf {U}}({\textbf {d}}) = \emptyset \). Next, we discuss Verse functions for verification via reachability.

Verification Algorithms in Verse. The Verse library comes with several built-in verification algorithms, and it provides functions that users can use to implement powerful new algorithms. We describe the basic algorithm and functions in this section.

Consider a scenario \({SC}\) with k agents and the corresponding hybrid automaton \({H}({SC})\). For a pair of modes, \({\textbf {d}},{\textbf {d}} '\) the standard discrete \({post} _{{\textbf {d}},{\textbf {d}} '}:{\textbf {X}}\rightarrow {\textbf {X}}\) and continuous \({post} _{{\textbf {d}},\delta }:{\textbf {X}}\rightarrow {\textbf {X}}\) operators are defined as follows: For any state \({\textbf {x}}, {\textbf {x}}' \in {\textbf {X}}\), \({post} _{{\textbf {d}},{\textbf {d}} '}({\textbf {x}}) = {\textbf {x}}'\) iff \({\textbf {x}}\in {\textbf {G}}({\textbf {d}},{\textbf {d}} ')\) and \({\textbf {x}}'={\textbf {R}}({\textbf {d}},{\textbf {d}} ')({\textbf {x}})\); and, \({post} _{{\textbf {d}},\delta }({\textbf {x}}) = {\textbf {x}}'\) iff \(\forall i\in {1,...,k}\), \({\textbf {x}}_i'={F}_i({\textbf {x}}_i, {\textbf {d}} _i, \delta )\). These operators are also lifted to sets of states in the usual way. Verse provides postCont to compute \({post} _{{\textbf {d}},\delta }\) and postDisc to compute \({post} _{{\textbf {d}},{\textbf {d}} '}\). Instead of computing the exact post, postCont and postDisc compute over-approximations using improved implementations of the algorithms in [14]. Verse’s verify function implements a reachability analysis algorithm using these post operators. The algorithm constructs an execution tree \({Tree} = \langle {V},{E} \rangle \) up to depth m in breadth first order. Each vertex \(\langle {\textbf {S}}, {\textbf {d}} \rangle \in {V} \) is a pair of a set of states and a mode. The root is \(\langle {\textbf {X}}^0, {\textbf {d}} ^0\rangle \). There is an edge from \(\langle {\textbf {S}}, {\textbf {d}} \rangle \) to \(\langle {\textbf {S}}', {\textbf {d}} '\rangle \), iff \({\textbf {S}}' = {post} _{{\textbf {d}} ',\delta }({post} _{{\textbf {d}},{\textbf {d}} '}({\textbf {S}}))\). The safety conditions are checked when the tree is constructed. Currently, Verse implements only bounded time reachability, however, basic unbounded time analysis with fixed-point checks could be added following [14, 32].

5 Experiments and Use Cases

We evaluate key features and algorithms in Verse through examples. We consider two types of agents: a 4-d ground vehicle with bicycle dynamics and the Stanley controller [22] and a 6-d drone with a NN-controller [23]. Each of these agents can be fitted with one of two types of decision logic: (1) a collision avoidance logic (CA) by which the agent switches to a different available track when it nears another agent on its own track, and (2) a simpler non-player vehicle logic (NPV) by which the agent does not react to other agents (and just follows its own track at constant speed). We denote the car agent with CA logic as agent C-CA, drone with NPV as D-NPV, and so on. We use four 2-d maps (\(\mathcal {M}1\)-4) and two 3-d maps \(\mathcal {M}5\)-6. \(\mathcal {M}1\) and \(\mathcal {M}2\) have 3 and 5 parallel straight tracks, respectively. \(\mathcal {M}3\) has 3 parallel tracks with circular curve. \(\mathcal {M}4\) is imported from OpenDRIVE. \(\mathcal {M}6\) is the figure-8 map used in Sect. 2.

Safety Analysis with Multiple Drones in a 3-d Map. The first example is a scenario with two drones—D-CA agent (red) and D-NPV agent (blue)—in map \(\mathcal {M}5\). The safety assertion requires agents to always separate by at least 1 m. Figure 4(left) shows the computed reachable set, its projection on x-position, and on z position. Since the agents are separated in space-time, the scenario is verified safe. These plots are generated using Verse ’s plotting functions.

Fig. 4.
figure 4

Left to right: (1) Computed reachtubes for a 2-drone scenario; (2) same reachtube projected on x-dimension, and (3) on z-dimension. Since there is no overlap in space-time, no collision. (4) Reachtube for a 3-drone scenario, the red drone violates the safety condition by entering the unsafe region after moving downward. (Color figure online)

Full size image

Checking Multiple Safety Assertions. Verse supports multiple safety assertions specified using \(\texttt {assert}\) statements. For example, the user can specify unsafe regions (Line 77–78) or safe separation between agents (Line 79–82) as shown in Fig. 5. We add a second D-NPV to the previous scenario and both safety assertions. The result is shown in the rightmost Fig. 4. In this scenario, D-CA violates the safety property by entering the unsafe region after moving downward to avoid collision. The behavior of D-CA after moving upward is not influenced. There is no violation of safe separation. Verse allow users to extract the set of reachable states and mode transitions that leads to a safety violation.

Fig. 5.
figure 5

Safety assertions for three drone scenario.

Full size image

Changing Maps. Verse allows users to easily create scenarios with different maps and port agents across compatible maps. We start with a scenario with one C-CA agent (red) and two C-NPV agents (blue, green) in \(\mathcal {M}1\). The safety assertion is that the vehicles should be at least 1m apart in both x and y-dimensions. Figure 6(left) shows the verification result and safety is not violated. However, if we switch to map \(\mathcal {M}3\) by changing one line in the scenario definition, a reachability analysis shows that a safety violation can happen after C-CA merges left Fig. 6(center). In addition, Verse allows importing map from OpenDRIVE [4] format. An example is included in the extended version of the paper [26].

Fig. 6.
figure 6

Left: running the three car scenario on map with parallel straight lanes. Center: same scenario with a curved map. Right: same scenario with a noisy sensor. (Color figure online)

Full size image

Adding Noisy Sensors. Verse supports scenarios with different sensor functions. For example, the user can create a noisy sensor function that mimics a realistic sensor with bounded noise. Such sensor functions are easily added to the scenario using the \(\texttt {set\_sensor}\) function.

Figure 6(right) shows exactly the same three-car scenario with a noisy sensor, which adds \(\pm 0.5\) m noise to the perceived position of all other vehicles. Since the sensed values of other agents only impacts the checking of the guards (and hence the transitions) of the agents, Verse internally bloats the reachable set of positions for the other agents by \(\pm 0.5\) while checking guards. Compared with the behavior of the same agent with no sensor noise (shown in yellow in Fig. 6(right)), the sensor noise enlarges the region over which the transition can happen, causes enlarged reachtubes for the red agent.

Plugging in Different Reachability Engines. With a little effort, Verse allows users to plug in different reachability tools for the postCont computation. The user will need to modify the interface of the reachability tool so that given a set of initial states, a mode, and a non negative value \(\delta \), the reachability tool can output the set of reachable states over a \(\delta \)-period represented by a set of timed hyperrectangles. Currently, Verse implements computing \(\texttt {postCont} \) using DryVR [14], NeuReach [35] and Mixed Monotone Decomposition [12]. A scenario with two car agents in map \(\mathcal {M}1\) verified using NeuReach and DryVR is included in the extended version of the paper [26].

Incremental Verification. We implemented an incremental verification algorithm in Verse called verifyInc. This algorithm improves verify by caching and reusing reachtubes, and can be effective when analyzing a sequence of slightly different scenarios. The function verifyInc avoids re-computing \({post} _{{\textbf {d}},{\textbf {d}} '}\) and \({post} _{{\textbf {d}},\delta }\) when constructing the execution tree by reusing earlier execution runs. Experiments show that verifyInc reduces running time by 10x for two identical runs and 2x when the decision logic is slightly modified. (More details are provided in the extended version of paper [26]). This exercise illustrates a usage of Verse in creating alternative analysis algorithms.

Table 1 summarizes the running time of verifying all the examples in this section. We additionally include three standard benchmarks: van-der-pol (Agent V) [20], spacecraft rendezvous (Agent S) [20], and gearbox (Agent G) [2]. As expected, the running times increase with the number of discrete mode transition. However, for complicated scenario with 7 agents and 37 transitions, the verification can still finish in under 6 mins, which suggests some level of scalability. The choice of reachability engine can also impact running time. For the same scenario in rows 2, 3 and 10, 11, Verse with NeuReachFootnote 2 as the reachability engine takes more time than using DryVR as the reachability engine.

Table 1. Runtime for verifying examples in Sect. 5. Columns are: number of agents (#\(\mathcal {A}\)), agent type (\(\mathcal {A}\)), map used (Map), reachability engine used (\(\texttt {postCont} \)), sensor type (N\(\mathcal {S}\)), number of mode transitions #TR, and the total run time (Rt). N/A for not available.
Full size table

6 Related Work

Automatic hybrid verification tools typically require the input model to be written in a tool-specific language [10, 13,14,15, 17, 25]. Libraries like JuliaReach [7] Hylaa [5] and HyPro [8] share our motivation to reduce the usability barrier by providing reachability analysis APIs for popular programming languages. Verse is distinct in this family in that it supports creation and analysis of multi-agent scenarios. The work in [33] also supports multiple agents, however, Verse significantly improves usability with maps, scenarios and decision logics written in Python.

Interactive theorem provers have been used for modeling and verification of multi-agent and hybrid systems [16, 19, 27, 29]. KeYmeraX [19] uses quantified differential dynamic logic for specifying multi-agent scenarios and supports proof search and user defined tactics. Isabelle/HOL [16], PVS [27], and Maude [29] have also been used for limited classes of hybrid systems. These approaches are geared for a different user segment in that they provide higher expressive and analytical power to expert users. Verse is inspired by widely used tools for simulating multi-agent scenarios [9, 18, 28, 30, 36]. While the models created in these tools can be flexible and expressive, currently they are not amenable to formal verification.

7 Conclusions and Future Directions

In this paper, we presented the new open source Verse library for broadening applications of hybrid system verification technologies to scenarios involving multiple interacting decision-making agents. There are several future directions for Verse. Verse currently assumes all agents interact with each other only through the sensor in the scenario and all agents share the same sensor. This restriction could be relaxed to have different types of asymmetric sensors. Functions for constructing and systematically sampling scenarios could be developed. Functions for post-computation for white-box models by building connections with existing tools [1, 10, 15] would be a natural next step. Those approaches could obviously utilize the symmetry property of agent dynamics as in [32, 34], but beyond that, new types of symmetry reductions should be possible by exploiting the map geometry.