We present multi-agent timed models, called MAPTs, where each agent is associated with a regular timed schema upon which all possible actions of the agent rely. MAPTs allow for a layered structure of the state space, so that it is possible to explore the latter dynamically and use heuristics to greatly reduce the computation time needed to address reachability problems. We then use an available tool for the Petri net implementation of MAPTs, to explore the state space of autonomous vehicle systems and compare this exploration with timed automata-based approaches in terms of expressiveness of available queries and computation time.
In this paper we propose models and methods tailored for e cient model-checking
of multi-agent systems composed of periodic communicating autonomous agents
evolving in a constrained environment. Typical examples of such systems are
systems of Communicating Autonomous Vehicles (CAVs), where each vehicle
(agent) observes its environment (the road, the other vehicles) and periodically
evaluates its environment in order to make a decision on the action to perform.
The decision policies of CAVs often rely on trajectory planning algorithms
studied in 3D simulation, sometimes in conjunction with on-road experiments [
Therefore, various properties of such systems are of interest to study safety, e ciency and robustness of the decision choices when some variability is introduced in the reaction times, transmission delays, etc. They can be either Boolean ones (e.g. Does some vehicle overtake another one before some milestone? Is a collision possible for a given safety distance?) or numerical ones (e.g. What is the minimal distance between two vehicles? What is the biggest deceleration for
Copyright c 2020 for the individual papers by the papers' authors. Copyright
c 2020 for the volume as a collection by its editors. This volume and its papers are
published under the Creative Commons License Attribution 4.0 International (CC BY
4.0).
some vehicle?). This motivates the use of formal methods and several approaches
exist focusing on the properties of vehicles (functional layer [
The framework VerifCar [
A closer look at the state spaces in the applications studied with VerifCar shows that they take the form of a directed acyclic graph (DAG). Each agent also has syntactically the form of a DAG between clock resets, and various forms of agents' communications are modelled through shared variables. Our goal is then to exploit these peculiarities to build a dedicated checking environment for reachability problems, when the models satisfy the kind of restricted forms we observed for CAV systems (as well as some other application domains). The hope is that this will allow to get rid of the uncomfortable restrictions we observed on the kind of queries that may be solved, while allowing to do it e ciently. Our aim is thus to change the balance between the expressiveness of the models and the richness of the queries while keeping a reasonable e ciency.
Concretely, we want to explore the state graph dynamically (checking temporal logic properties and computing numerical indicators directly as we explore states) to avoid constructing the full state space, and therefore not to loose time and memory space storing and comparing all previously reached states. The objective is to be able to tune the veri cation algorithm with heuristics that will choose which path to explore in priority, which might signi cantly speed up the computation time if the searched state exists. That implies that our algorithms should explore the graph depth- rst, since breadth- rst algorithms cannot explore paths freely and are restricted to fully explore all the states at some depth before exploring the next one.
For systems featuring a high level of concurrency between actions, such as the CAV systems, most of the non-determinism results from possibly having several actions of di erent agents available from a given state, that can occur in di erent orders and which often lead eventually to the same state. This corresponds in the state space to what is sometimes called diamonds. Breadth- rst exploration allows to compare states at a given depth and therefore remove duplicates. On the other hand, depth- rst exploring such a state space with diamonds, leads to examine possibly several times the same states or paths, which is not e cient. In this context, our aim is to detect and merge most identical states coming from diamonds while continuing to explore the state space mainly depth- rstly. This diamond detection will consist in a breadth- rst exploration in a certain layer of the state space, each layer corresponding to some states at a given depth having common characteristics. It turns out that such layers are typically observed in the state spaces of CAV systems. This allows for a depth- rst exploration from layer to layer, while greatly reducing the chances of exploring several times the same states. The class of models on which this kind of algorithm can be applied will be referred to as Multi-Agent with timed Periodic Tasks (MAPTs).
In order to analyse a model, it is useful to translate it into formalisms
for which we have existing tools. Like in [
The existing works on state space reduction such as [
Other approaches, using bounded model checking [
Concerning the exploration algorithms, since the systems we aim to model
with MAPTs produce acyclic state spaces, this allows us to use more e cient
on-the- y algorithms for CTL than those proposed in the literature for general
cases, such as [
In this paper, we start with a formal de nition of MAPT, give some examples and provide a translation to high-level Petri nets. Then, we present the exploration algorithms taking advantage of the layered structure, weak and strong variables, and heuristics. Finally, we use MAPT in experiments that highlight the bene ts of our approach in terms of expressiveness of available queries and computation time, and compare them with VerifCar when possible. The contributions of the paper are the introduction and analysis of the MAPTs, as well as the e cient exploration method dedicated to this new formalism. 2
We rst de ne G-MAPTs, composed of several agents that may interact through shared variables. Each agent is associated with a unique local clock and performs actions occurring in some given time intervals. There is no competition between agents in the sense that no agent will ever have to wait for another one's action in order to perform its own actions. However, there may be non-determinism when several actions are available at the same time, as well as choices between actions and time passing.
A G-MAPT is a tuple (V; F; A; Init) where: { V is a set of values; { F is a ( nite) set of calculable functions from V to V; { A is a set of n agents such that 8i 2 [1; n], agent Ai =df (Li; Ci; Ti; Ei) with: Li is a set of localities denoted as a list Li =df (li1; : : : ; limi ) with mi > 0, such that 8i 6= j, Li \ Lj = ;; Ci is the unique clock of agent Ai, with values in N (we assume Ci 6= Cj if i 6= j, but they may have the same value); Ti is a nite set of transitions, forming a directed acyclic graph between localities, with a unique initial locality li1 and a unique nal locality limi , each transition being of the form (l; f; I; l0) where l; l0 2 Li are the source and destination localities, f 2 F is a transformation function and I =df [a; b] is an interval with a; b 2 N and a b;
Ei 2 N n f0g is the reset period of agent Ai. { Init is a triple (ini!tL; init!C ; initV ) = ((l1; ; ln); (init1; ; initn); initV ) where 8i 2 [1; n], li 2 Li, initi 2 N and initV 2 V.
For each agent Ai and each locality l 2 Li, we shall de ne by l = f(l; f; I; l0) 2 Tig the set of transitions originated from l, and by l = f(l0; f; I; l) 2 Tig the set of transitions leading to l. We assume that li1 = ; and (limi ) = ;. Moreover, when i 6= j, since Li \ Lj = ;, Ti \ Tj = ; too, so that each transition belongs to a single agent, avoiding confusions in the model. A simple example of a G-MAPT M with two non-deterministic agents is represented in Ex. 1.
In the semantics, for each agent Ai, we emulate a transition ri from limi to li1 that resets clock Ci every Ei time units. As such, each agent in the network cycles over a xed period. There can be several possible cycles though, since a given locality may be the source of several transitions, so that there may be several paths from li1 to limi . The behaviour of the system is de ned as a transition system where Init is the initial state. A state of a G-MAPT composed of n agents is a tuple denoted by s = (l; c; v) where l = (l1; ; ln) with li 2 Li the current locality of agent Ai, c = (c1; ; cn) where ci 2 N is the value of clock Ci, and v 2 V. We shall sometimes consider that v is the value of some shared variable V used to model the evolution of the system.
There are three possible kinds of state changes: a ring of a transition, a clock reset and a time increase. From the state s = (l; c; v): { A transition (l; f; [a; b]; l0) 2 Ti can be red if li = l and a ci b. Then, in the new state, li l0 and V f (v). { For any agent Ai, clock Ci can be reset if li = limi and ci = Ei. Then, Ci 0 and li li1. { Time can increase if 8i 2 [1; n], either there exist at least one transition (l; f; [a; b]; l0) 2 Ti with li = l and ci < b, or li = limi and ci < Ei. A time increase means that 8i 2 [1; n], Ci ci + 1.
The transition system associated with a G-MAPT is driven by these state changes, from the initial state. It may be observed that there is a single shared element in such a system: variable V ; all the other ones are local to an agent. It is unique but its values may have the form of a vector, and an agent may modify several components of this vector through the functions of F used in its transitions, thus emulating the presence of several shared variables. The values of V are not restricted to the integer domain, but there is only a countable set of values that may be reached: the ones that may be obtained from initV by a recursive application of functions from F (V is not modi ed by the resets nor the time increases). However this domain may be dense inside the reals, for instance. Example 1. Let M = (V; F; A; Init) where: { V = R
N;
f1(x; y) ! (2x; y + 1) { F = ff1; f2; f3; f4g with f3(x; y) ! ( x2 ; y) { A = f(L1; C1; T1; E1); (L2; C2; T2; E2)g with
L1 = f1; 2g T1 = f(1; f1; [1; 2]; 2); (l; f2; [3; 3]; 2)g E1 = 5
L2 = f3; 4g T2 = f(3; f3; [1; 2]; 4); (3; f4; [3; 3]; 4)g E2 = 5 { Init = ((1; 3); (0; 0); (0:5; 0)).
A visual representation of M and the initial fragment of its dynamics is depicted in Fig. 1.
G-MAPT semantics when considered in a naive way is prone to a state space explosion phenomenon. Motivated by our target applications, we restrict G-MAPTs with Assumption 1 to produce state spaces being DAGs. Assumption 1 (acyclicity of the state space) 1. V may be promoted into a partially ordered set (V; <) and there exist an agent Ai such that, in all paths from li1 to limi in the local graph of Ai (see for example Fig. 1), there exists a transition t =df (l; f; [a; b]; l0) such that for all v 2 V, v < f (v); in general, V = W X, where (X; <) is a known ordered set and the order is extended in a natural way to V by stating that (w; x) < (w0; x0) i x < x0; f2(x; y) ! (x + 1:3; y + 1) f4(x; y) ! (2x; y) [3; 3] f2 2. and there is no f 2 F such that for some v 2 V, we have f (v) < v.
Item 1 ensures that at least one agent increments the variable V at least once between two of its resets.
Item 2 ensures that no function can decrease the variable V . The result is an absence of cycles in the whole state space of the G-MAPT.
Furthermore, in order to shorten the computation time of the queries, we also
consider an accelerated semantics that often allows to increase time by several
time units in one step. We shall not detail it here (see [
maxfb j (l0; f; [a; b]; l) 2 lg minfb0 j (l; f 0; [a0; b0]; l00) 2 l g; 4. and we have maxfb j (l0; f; [a; b]; limi ) 2 limi g Ei.
Items 1 and 2 ensure that, when the system is started, either in the terminal locality or in a non terminal one of some agent, the time is not blocked and we shall have the possibility to perform an action in some future.
Item 3 ensures that whenever a non terminal locality is entered, any (and not only some) transition originated from that locality will have the possibility to occur in some future (the case when we enter an initial locality is irrelevant since resets reinitialise the corresponding clock to 0).
Item 4 captures similar features in the case when we enter a terminal locality. In other words, each transition or reset in l is enabled when entering l or will be enabled in the future (after possibly some time passings in order to reach the lower bound a).
De nition 2. A MAPT is a G-MAPT satisfying Assumptions 1 and 2. 3
A high-level Petri net [
Formally, a high-level Petri net is a tuple (S; T; ; M0) where: { S is a nite set of places; { T is a nite set of transitions; { is a labelling function on places, transitions and arcs such that for each place s 2 S, (s) is a set of values de ning the type of s, for each transition t 2 T , (t) is a Boolean expression with variables and constants de ning the guard of t and for each arc (x; y) 2 (S T ) [ (T S), (x; y) is the annotation of the arc from x to y, driving the production (on y, when x 2 T and y 2 S) or consumption (from x, when x 2 S and y 2 T ) of tokens (see an example below). { M0 is an initial marking associating tokens to places, according to their types: for each s 2 S, M0(s) is a nite multiset of values in (s).
The semantics of a high-level Petri net is captured by a transition system containing as states all the markings which are reachable from the initial marking M0. A marking M 0 is directly reachable from a marking M if there is a transition t enabled at M , whose ring leads to M 0; it is reachable from M if there is a sequence of such rings leading to it. A transition t is enabled at some marking M if the tokens in all the input places of t allow to satisfy the ow expressed by the annotations of input arcs and the guard of t, through a valuation of the variables involved in the latter. The ring of t consumes the concerned tokens in input places of t and produces tokens on output places of t, according to the annotations of the output arcs and the same valuation, as shown below for a transition before and after the ring.
s1 1 s2 2 y x x > 0 (w; z) t
(0; 0) (w + x; z + y) s3 s1 s2 y x x > 0 (w; z) t (w + x; z + y) s3 (1; 2) 3 We shall allow in nite value sets, but there will never be in nitely many tokens in the system
De nition 3. Given a G-MAPT Q = (V; F; A; Init) with jAj = n, its translation to a high-level Petri net N = translate(Q) = (S; T; ; M0) is de ned as follows: { S = fsA; sC ; sV g with (sA) =df L1 Ln where Li is the set of localities of agent Ai (its jth element is denoted lij ), (sC ) =df Nn and (sV ) =df V. For any token x of the type (sA) or (sC ), x[i] is the ith element of the list. { T =df Ttrans [ Treset [ fttimeg where
Ttrans is the smallest set of transitions such that, for each agent Ai = (Li; Ci; Ti; Ei) in A and for each transition (l; f; [a; b]; l0) 2 Ti, there is a transition t 2 Ttrans such that (sA; t) =df x, (sC ; t) =df y, (sV ; t) =df z, (t; sA) =df x0 where x0[i] l0 and 8j 6= i, x0[j] x[j], (t; sC ) =df y, (t; sV ) =df f (z) and (t) =df (x[i] = l) ^ (a y[i] b). This is equivalent to the set of transitions of the G-MAPT.
Treset is the smallest set of transitions such that, for each agent Ai = (Li; Ci; Ti; Ei) in A, there is a transition t 2 Treset such as (sA; t) =df x, (sC ; t) =df y, (t; sA) =df x0 where x0[i] li1 and 8j 6= i, x0[j] x[j], (t; sC ) =df y0 where y0[i] 0 and 8j 6= i, y0[j] y[j], and (t) =df (x[i] = limi ) ^ (y[i] = Ei) where mi =df jLij. This is equivalent to the set of clock resets of the G-MAPT.
(sA; ttime) =df x, (sC ; ttime) =df y, (ttime; sA) =df x, (ttime; sC ) =df y0, where 8i 2 [1; n], y0[i] y[i] + 1, and (ttime) =df G1 ^ ^ Gn where Gi acts as the "upper bound guard" for all the transitions in agent Ai, i.e., Gi =df (g1 _ _ gmi ) with mi = jLij and 8j 2 [1; mi 1], gj =df (x[i] = lij ) ^ (y[i] < B), where B = maxfbj(lij ; f; [a; b]; l0) 2 lij g is the highest upper bound of the intervals from all outgoing transitions of lij and gmi =df (x[i] = limi )^(y[i] < Ei). This is equivalent to a time increase. { (M0(sA); M0(sC ); M0(sV )) = Init is the initial marking
The translation associates singletons as arc annotations for all arcs. As a consequence, during the execution, starting from the initial marking which associates one token to each place, there will always be exactly one token in each of the three places. Each reachable marking, where sA contains l, sC contains c and sV contains v, encodes a state (l; c; v) of the considered G-MAPT.
It is easy to see [
When model checking a system, one usually has the choice between a depth- rst and a breadth- rst exploration of the state space. For reachability properties (where one searches if some state satisfying a speci c property may be reached), depth- rst (directed and limited by the query) is usually considered more effective. However, the majority of the non-determinism in systems featuring a high level of concurrency (such as CAV systems) leads to diamonds. Indeed, if transitions on di erent agents are available at a state then they may occur in several possible orders, all of them converging most of the time to the same state (if the applied functions commute). In order to avoid exploring again and again the same states, a depth- rst exploration needs to store all the states already visited up to now, which is usually impossible to do in case of large systems. For example, if states s1 and s2 share a common successor s3, when the algorithm will compute the successors of s1, it will classically remove s1 from the stack and continue with its successors, until reaching s3 and exploring all paths from s3, forgetting each time the nodes already visited. That way, when the algorithm has explored all paths from s1 and starts exploring from s2, there is no memory of s3 having been explored already, and thus all paths starting from it will be explored again.
On the contrary, using breadth- rst algorithms would partly allow to avoid that issue, because duplicate states obtained at a given depth can be removed. However, this would also imply exploring all reachable states at a given depth and forbid using heuristics to guide and limit the exploration.
An idea is then to combine both approaches, which is possible for MAPTs, using the layered approach described next. A MAPT may be non-deterministic but it is strongly live and has a DAG state space. For instance, the G-MAPT M from Ex. 1 satis es both assumptions (acyclicity is satis ed due to y being incremented in all cycles of A1) and so is actually a MAPT. 4.1
The state space of a MAPT shows an interesting characteristics: apart from having no cycles, its structure can often be divided in layers such that all states on the border of a layer share the same vectors of localities and clocks (and thus, the same set of enabled transitions) and are situated at the same time distance from the initial state. The only di erence concerns the value of the variable, due to the non-determinism and the concurrency inherent to this kind of models. Non-determinism means that an agent has the choice between several transitions at some location; concurrency means that at least two agents may perform transitions at some point. In the rst case, several paths may be followed by the agent to reach some point, leading to di erent values of the variable; in the second case, transitions of the two agents may be commuted, leading again to di erent values of the variable if the corresponding functions do not commute.
For instance, if agent Ai in a MAPT starts at li1 with a null clock, after Ei time units and before (Ei + 1) time units, it shall necessarily pass through its reset (it is possible that it performs other transitions before and/or after this reset without modifying its clock, but it is sure the agent will go through this reset before performing a new time passing). Hence, if each agent starts from its initial locality with a null clock, after lcmfE1; : : : ; Eng (i.e., the least common multiple of the various reset periods; denoted in the following by lcm(E)) time units, it is sure we shall revisit the initial localities with null clocks, but possibly with other values of the variable V , yielding the border of a layer. From this border the same sequences of transitions/resets/time-passings as initially will occur periodically (with a period of lcm(E)), leading to new borders, with the initial localities and the null clocks.
Exploring layered state space The function N extBorder(state) takes a state (l; c; v) and computes, through a breadth- rst exploration, the set of successors up to the next border. To do so we introduce a function N extState(s), which returns the set of all successors of state s. This is used iteratively in a depth- rst exploration to jump from a state to one of its successors belonging to the next border. During this exploration, an additional function may be used to check if a visited state satis es some condition. Such a use of layers allows to reduce the number of explored paths by detecting diamonds caused by the order of transitions of concurrent agents.
Exploration using strong and weak variables The approach presented above does not deal with diamonds spreading on a time distance longer than the one between two adjacent borders. For example, it may still happen that two di erent states s1 and s2 belonging to the same border have a common successor s in the future. To cope with this issue, it is more interesting to perform the breadthrst exploration that computes successors at the next border for the set fs1; s2g instead than taking them separately. In general, it is not obvious to know or guess which states should be kept together in the computation of the next border. Indeed, one should be able to determine when sets of states should be split in sub-sets and when they should be kept together. To perform such a clustering, it may be interesting to exploit the properties of target applications, such as CAVs.
A possible solution is to assume V =df Vw Vs, where Vw (weak) is a "less important" part of V and Vs (strong) a "more important" one, such that states di ering in the valuation of Vs are unlikely to have a common successor, while this is not the case for Vw. Symmetrically, states with the same valuation of Vs are more likely to have a common successor. This may give us a criterion to cluster states and jump from a set of states to the set of their successors at the next border. The choice of Vs and Vw is of course system-dependent and should be de ned by an expert, or with the help of a simulation tool. As an example, elements that can be assigned a new value independently of their previous one might be considered as weak, while elements whose value changes depend on their present value (for instance the position of a moving object) might be considered as strong.
The function ClusteredN extBorder(state set) is then an easy variant of N extBorder(state), taking a set of states and producing a set of clusters, i.e., sets of states having identical values of variables in Vs. It is used in a similar way as N extBorder() to explore in a depth- rst manner the layered state space, the only di erence being that it jumps from a cluster belonging to some border to a cluster belonging to the next one, based on the choice of Vs.
This section is dedicated to exploration algorithms of nite pre xes of MAPTs: states that do not have successors in the considered pre x will be called nal. The algorithms are denoted with the CTL temporal logic syntax. Since this temporal logic is meant to explore in nite paths, we shall consider that each nal state has a self loop.
Our algorithms have two main characteristics: they operate "on-the- y", which means that they do not store the entire visited state space (but only a cut of it), and they can be tuned with heuristics de ning a priority on paths to be explored, that might signi cantly speed up the computation time if the searched states exist. To do so we rely on the procedure ClusteredN extBorder() mentioned above. Since our algorithms do not store all the states that have been explored, we do not return traces of execution, unlike what is usually proposed by standard temporal logic model checking tools.
Although the general case for checking reachability CTL formulas has not yet been implemented (left for a future work), it can be done easily thanks to the absence of cycles in the state space. Here, we shall present the algorithms used in our experiments. The atomic formulas p can be any Boolean formula using variables or current localities of the state where p is checked. It is also possible to use clock values, but only with the original semantics: the accelerated semantics reduces the state space in a way that preserves the sequences of transitions, but not all the clock values.
The algorithm for EF p (meaning a reachable state satis es p) consists, starting from a stack containing the initial state, in taking the rst element s of the stack, returning it if p is true on s, and otherwise adding the result of ClusteredN extBorder() to the stack. The algorithm continues recursively until reaching p or there is no more states to explore in the considered nite pre x. Additionally, we return true if p is satis ed by a state between two borders, i.e., during an application of ClusteredN extBorder().
The algorithm for EGp (meaning there exists a path where p is always true) works in a similar way, but the state s is returned if p is true on s and if s is nal, and ClusteredN extBorder(s) is added to the stack only if p is true on s. Additionally, states where p is not true are dropped when explored in ClusteredN extBorder(). That way, only states where p is true are explored.
We shall also describe how to check nested CTL queries, of the kind EF (p ^ EF q), meaning that a reachable state satis es p and from that state a reachable state satis es q, and EF (p^EGq), meaning that a reachable state satis es p and from that state there exist a path where q is always true. Those nested queries are implemented using a marking function (i.e., a Boolean indicator). EF (p ^ EF q) is implemented as follows. Whenever p is true on a state, the state is marked. Whenever a state is marked, all its successors are marked. Starting from a stack containing the initial state, the rst element s of the stack is returned if q is true on s and s is marked. Otherwise, the result of ClusteredN extBorder(s) is added to the stack. The same marking process is performed between two borders, i.e., in ClusteredN extBorder(). We continue recursively until a state validates the property or there is no more state to explore. As for EF (p ^ EGq), states are marked whenever both p and q are true or the state is a successor of a marked state and q is true. If a marked nal state is reached, it validates the property and is returned. Again, the same marking process is performed in ClusteredN extBorder().
To have a better idea of how those algorithms are implemented, we provide Algorithm 1 computing EF (p ^ EGq).
Algorithm 1 EF (p ^ EGq) exploring:add(init) fadd initial state to the stack of states to exploreg while exploring do successors N extBorder(exploring:pop()) fremoves the state at the end of the stack and store all its successorsg for all s 2 successors do if (check(p; s) or parent marked(s)) and check(q; s) then mark(s) fs is marked if either p is true on s or q is true on s and its predecessor is markedg end if if is marked(s) and check(f inal; s) then
return true freturns true if s is a marked nal stateg else if not check(f inal; s) then
exploring:add(s) fotherwise and if s is not a nal state, add it to the stackg end if end for end while return false 5
In this section we illustrate the performances of our exploration algorithms
applied to three models used in [
More speci cally, we assume that the road section is composed of three unidirectional lanes the vehicles move on, and we store at any time the coordinates (position) of each vehicle on it. Each vehicle is represented by a rectangle with a given length and width, centered on its position. Its state is thus described by a record containing its position, current longitudinal and lateral speeds, longitudinal acceleration (in a given range from negative to positive values), current direction and knowledge about intentions of other vehicles (for example in the form of timed trajectories).
Since we are focusing on the e ciency and robustness of decision choices and not on the control of vehicles (i.e., the module responsible for producing a trajectory according to the decision choices), we abstract from the physical laws involved in a maneuver such as rotation or inertia. In other words, we assume that turning the steering wheel impacts the speed value that will make the rectangle move on the x-axis, while its longitudinal speed still makes it move on the y-axis.
At a constant frequency of 10 Hz, the speed and position of each vehicle is updated by a transition of an agent environment update.
We assume that the vehicles (1) observe the behavior of their neighbors and that the information obtained from the perception sensors is always accurate and immediate and (2) communicate and receive pieces of information, which are not directly observable, such as the planned lane change of the other vehicles; these communications are timed in order to realistically represent the delays between emissions and receptions of data. The behavior of each vehicle consists in repeating endlessly, at its own constant frequency: { a computation allowing to make a decision on the immediate action to be performed (i.e., execution of the decision algorithm) in the form of an acceleration (speed increase, braking, no change) and a direction (left, right, no change), followed by { the communication of its own intention (in the form of the trajectory it wishes to follow) to all vehicles (close enough to be) able to receive this information. Received information coming from the other vehicles is stored in the database of the vehicle and used when running the decision algorithm.
A decision algorithm has been implemented for the experiments [
In the following, we rst discuss the advantages and drawbacks of using
various types of layer-based explorations. Then, we provide some heuristics, and
experiment them in order to (hopefully) observe the gain that can be achieved
with them. Finally, we compare this method with the framework VerifCar [
E
ciency of the layer-based exploration.
Here, we compare, for several exploration algorithms, the full exploration time and the reachability time of the rst occurrence of a nal state. They are explored in breadth- rst, depth- rst without layers and depth- rst with layers (with and without the use of strong/weak variables). The sizes of the state spaces for Models 1, 2 and 3 are respectively of 7751, 52732 and 285944 states.
Exploration algorithm Breadth rst Depth- rst without layers Depth- rst layered (Vw = ;) Depth- rst layered (small Vw) Depth- rst layered (large Vw)
Full exploration time (s) Model 1 Model 2 Model 3 10:8 52:1 420
As shown in Table 1, one can see that the breadth- rst algorithm has the best full exploration time in any case, but the time before reaching any nal state is close to the full exploration one, which makes it the worst technique in this case. On the other hand, the standard depth- rst algorithm is the fastest for reaching a nal state, but it does not fully explore the state space even after 50 hours of computation.
Results for Model 1 show that as long as the layer based approach is used, the full exploration time is very close to that of the breadth- rst one. This indicates that there is almost no diamonds covering several layers, meaning that di erent states belonging to the border of a layer almost never share a common successor. For this reason the use of weak variables has no e ect. Although this case is rather simple, it clearly highlights the advantage of layer-based exploration: with almost no increase in full exploration time, it is able to reach a nal state much faster.
Model 2 and 3 have much more complex state spaces and, in both cases, the layer-based algorithm that does not rely on weak variables to aggregate states is not able to explore the full state space even after 50 hours of computation. On the contrary, using even a small number but well chosen weak variables (6 out of 39), it is possible to fully explore the state space. In both cases, exploration is about ve times longer than the exploration time of breadth- rst algorithm. When using a large number of weak variables (30 out of 39), the exploration is much shorter (about 1:5 times the time of breadth- rst algorithm). One can note however that the larger Vw, the longer it takes to reach a nal state. Indeed, as states are aggregated layer by layer, a too large Vw would result in an exploration similar to a breadth- rst one, where all states are kept together and nal states are only reached at the end of the computation. With the weak variables chosen, the time to reach a nal state remains however reasonable.
In the next experiments, the depth- rst algorithms always use layers and a xed non-empty Vw.
Exploration algorithms based on layers allow the use of heuristics. These heuristics guide the exploration, choosing among all the unexplored states the one that will most likely lead to a state that satis es the checked property. The heuristics we use associate a weight to each state, such that when a new state is discovered, it is placed in a list ordered by weight of states to explore. The weight is a prediction of the distance between the current state and a state satisfying the property.
Therefore, a reachability property may be associated with a heuristics that takes a state as an input and returns a weight as an output. Below is a list of heuristics that we used for experiment purposes together with the property they are associated with: 1. distance vh1 vh2 : returns the longitudinal position of vehicle vh1 minus that of vehicle vh2. It is used with property EF arrival vh1 bef ore vh2, where arrival vh1 before vh2 is true in a state if vehicle vh1 reaches the end of the road portion before vehicle vh2 does. The idea behind is to check in priority states where vh1 is the most ahead of vh2. 2. estimated travel time vh: returns the time traveled since the initial state4 plus the estimated time to reach the end of the road portion, assuming the current speed is maintained. It is used with property EF travel time vh sup n, where travel time vh n is true in a state if vh reaches the end of the road portion in n time units or more. The idea is to check in priority states where vh is predicted to reach the end of the road with the longest time. 3. time to overtake vh1 vh2 : is the time before both vehicles arrive at the same longitudinal position if they keep their current speed. It is used with property EF ttc vh1 vh2 n, where ttc vh1 vh2 is the value of the time to collision indicator between vh1 and vh2 (i.e., the delay before there is a collision between the two vehicles if they keep their current speed), and n is a time to collision value. The idea is to check in priority states where one of the vehicles is getting closer to the other one with the higher speed.
These heuristics have been used on Model 3, with results given in Table 2. The scenario in Model 3 considers three vehicles positioned as depicted in Fig. 2 on a two lane road portion that is 500 m long, with one additional junction lane. Initially, vehicle A is on the right lane at position 0 m with a speed of 30 m/s, vehicle B is on the left lane at position 30 m with a speed of 15 m/s and vehicle C is on the junction lane at position 40 m with a speed of 20 m/s. They all aim at being on the right lane at the end of the road portion.
The rst two queries (EF arrival B bef ore A and EF travel time A 15:9) can only be true in a nal state (the deepest layer). As such, the reachability time with the breadth- rst algorithm is close to the full exploration time with the same algorithm. In general, the breadth- rst reachablity time depends on 4 Elapsed time since initial state can be estimated by counting how many times an agent has returned to its initial locality. the depth of the rst state that satis es the property. One can observe that for the fourth query (EF ttc A B 0), the state is actually reached at a lower depth, which is re ected by the reachability time.
As the depth- rst algorithm without heuristics randomly chooses which paths to explore rst, the reachability time varies. The number of states in the whole state space that satis es the property thus impacts the mean reachability time with this algorithm, i.e., when there is more possibility to verify the property, the average time needed is shorter. As we do not want to rely on luck, this is not satisfying.
On the other hand, depth- rst algorithm with heuristics explores states in a given order (depending on their weights) and therefore the reachablity time is always the same. The heuristics we used could of course be modi ed and improved, but they are enough to show a signi cant decrease of the reachability time. Even for the fourth query, where the breadth- rst is faster than the depthrst algorithm, the heuristics allows to quickly identify the state that satis es the property.
We will now compare the reachability time obtained with Uppaal with the ones
obtained with the depth- rst exploration algorithms with heuristics, on Model 3.
We observed that Uppaal rst constructs the state space in about 106 s, then
is able to answer almost instantly if a searched state exists. It can therefore
answer several queries after constructing the state space, unlike our
heuristicsbased dynamic exploration algorithms, which have to explore the state space
from scratch for each query. Yet, most of the states we aimed for can be reached
easily, and the computation took only about 4 seconds. Queries depicted in
Table 2 are those where states were harder to reach. Compared to the ones
we obtained in [
However, Uppaal is restricted in terms of query language, at least in two
ways interesting for us. First, it is not possible to directly check bounds of a
given numerical indicator, and such bounds should be obtained by dichotomy,
requiring several runs for each indicator, such as proposed in the methodology
of [
Indeed it is possible to do a full exploration of the state space while keeping, for each state, the lower and higher values reached on the paths leading to the state, for a given set of indicators. That way, all the information needed to analyse the behaviour of the system, can be obtained after only one full exploration. This is performed as a standard breadth- rst exploration (storing states in a le) with the di erence that each state is associated with a set of pairs (min; max), being the (temporary) bounds of the considered indicators. Each time a state is explored, the value for each indicator is computed, and it overwrites min if it is smaller, and max if it is greater. That way, each state s contains, for each indicator, the smallest and highest values that exist on the paths from the initial state to s. As several paths can lead to s, we will consider that s reached from path P 1 and s reached from path P 2 are equivalent only if the set of their indicators are equal. Therefore, some diamonds might be detected (i.e., two identical states coming from di erent paths) but not merged together in order to keep information about their respective paths. That way it is possible to have several versions of the same state, but with di erent indicator values. If one is interested in the reachability of states (for instance, if an indicator is equal to some value), this can easily be done in the same way, by adding Boolean variables to the set of indicators. At the end of the exploration, we get this way the set of all nal states, together with all the information that has been carried on their respective paths. It therefore contains all the information needed to analyse nely the system. For the case of Model 3, getting the arrival order together with the bounds for travel time and worst time-to-collision takes 708 seconds. In comparison, the time needed by Uppaal to obtain the same information with the dichotomy procedure is 3553 seconds.
Also, the DAG shape of the state space allows us to implement nested CTL queries. For the experiments, we used a query of the kind EF (p ^ EGq), which is the negation of the "leads to" operator p > :q (the only nested operator available in Uppaal, in addition to deadlock tests) and two of the kind EF (p ^ EF q), which cannot be expressed in Uppaal.
In [
Finally, it is worth mentioning that discretisation is needed for Uppaal, and therefore approximations may be mandatory in some cases, leading to a loss in precision and realism. In addition to a better expressiveness, the model checking process presented in this paper also ensures that no approximation is needed, hence a higher level of realism is achieved. 6
We introduced G-MAPTs, multi-agent timed models where each agent is associated with a regular timed schema upon which all possibles actions of the agent rely. The formalism allows to easily model systems featuring a high level of concurrency between actions, where actions are not temporally deterministic, such as the CAVs. We have then formalised MAPTs (Multi-Agent with timed Periodic Tasks), by soundly constraining G-MAPT ones. We also presented how to extract a layered structure out of a MAPT, that allows to detect diamonds while exploring the system depth- rst. A translation from G-MAPT to highlevel Petri nets allowed us to implement a dedicated checking environment for this formalism with the (free) academic tool Zinc. Algorithms implemented in such environments explore state spaces dynamically and can be used together with heuristics that allow to reduce the computation time needed to reach some states in the model. Finally, experiments highlighted the e ciency of our abstractions, and a comparison of model checking CAVs systems with the framework VerifCar has been performed. Although our checking environment does not return traces of executions and is not better for full exploration times than the state of the art tool Uppaal used in VerifCar, it has a better expressiveness both on the model, since we can compute with non-integer numbers, and on the queries since nested CTL ones can be checked. The heuristics performed well for reachability problems and we also provided an exploration algorithm that allows to gather all information needed to analyse the system in one run, which greatly decreased the time needed to gather the same amount of information when using VerifCar. Although we developed this method with the case study of autonomous vehicles in mind, this formalism and all the abstractions and algorithms presented in this paper can be easily applied to any multi-agent real time systems where agents adopt a cyclic behaviour, such as mobile robots completing cyclically tasks according to their own objectives, ying drone squadrons, etc.