{'fraction_non_alphanumeric': 0.039848268609629686, 'fraction_numerical': 0.010140464207917074, 'mean_word_length': 4.323270691723311, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Introducing Liveness into Multi-lane Spatial Logic lane change controllers using UPPAAL

With Multi-lane Spatial Logic (MLSL) a powerful approach to formally reason about and prove safety of autonomous traffic manoeuvres was introduced. Extended timed automata controllers using MLSL were constructed to commit safe lane change manoeuvres on highways. However, the approach has only few implementation and verification results. We thus strenghen the MLSL approach by implementing their lane change controller in UPPAAL and confirming the safety of the lane change protocol. We also detect the unlive behaviour of the original controller and thus extend it to finally verify liveness of the new lane change controller.


Introduction
Nowadays, driving assistance systems and fully autonomously driving cars are increasingly capturing the market. For such autonomous systems, traffic safety and prevention of human casualties is of the utmost importance. In this context, safety means collision freedom and thus reasoning about car dynamics and spatial properties. A softer, but also highly desirable, requirement is liveness, meaning that a good state is finally reachable.
An approach to separate the car dynamics from the spatial considerations and thereby to simplify reasoning, was introduced in [13] with the Multi-lane Spatial Logic (MLSL) for expressing spatial properties on multi-lane motorways with one driving direction for all cars. The idea to separate dynamics from control laws follows the work by Raisch et al. [20] and Van Schuppen et al. [11].
The logic MLSL and its dedicated abstract model was extended for country roads with oncoming traffic [12] and urban traffic scenarios with intersecting lanes [14,27]. The authors informally introduced respective controllers for safe lane change manoeuvres and safe turning manoeuvres at intersections. The respective safety of the controllers is proven with a semi-formal mathematical proof [13,12,14]. With automotive-controlling timed automata (ACTA), a formal semantics for the previously informal controllers was later introduced [14]. (Un-) decidability results for (parts of) the logic MLSL were provided [10,16,23].
MLSL itself is a thoroughly researched and strong formal approach for proving properties of autonomous traffic manoeuvres. Recently, the first computer-based assistance for reasoning with a new hybrid extension of MLSL (HMLSL) was introduced by Linker [17]. The authors successfully investigate safety constraints for the motorway traffic scenarios from [13] with Isabelle/HOL [22]. They outline an interesting extension of their work to liveness properties.
In this paper, we also focus on the motorway case. While [17] presents a strong implementation result focused directly on the spatio-temporal logic HMLSL, we instead investigate safety and liveness of the protocol of the lane change controller for highway traffic [13]. The controller can be formalised as an automotive-controlling timed automaton (ACTA) [14] and uses formulas of MLSL to reason about traffic situations and to decide, whether a car can safely change lanes.
As ACTA are extended timed automata [1], we implement the lane change controller in the tool UPPAAL [2], which allows for model-checking of timed automata. With this, we verify the correct behaviour of the considered lane change protocol and confirm the hitherto informally proven safety property in a preferably generic UPPAAL model. Thus, our goal is to show unreachability of a bad state with a collision in the overall system. With UPPAAL, we also detect the absence of liveness in the original lane change controller from [13]. We thus adapt the old lane change controller and show the liveness of the new controller with UPPAAL.
In Sect. 2, we briefly introduce the abstract model and logic MLSL from [13]. We also introduce the lane change controller and ACTA formalism. In Sect. 3, we explain the adaptions of the lane change controller for the implementation in UPPAAL and introduce our UPPAAL verification properties. We extend the original controller from [13] to a new live lane change controller in Sect. 3.4. Finally, we summarise our results in Sect. 4 and give ideas for future work.

Preliminaries
In this section, we briefly introduce the approach from [13]. For this, we start with an overview over the abstract model for highway traffic in Sect. 2.1 and introduce the Multi-lane Spatial Logic in Sect. 2.2. In Sect. 2.3, we introduce the automotive-controlling timed automata (ACTA) from [14], which serve to formalise the lane-change controller from [13], that we describe in Sect. 2.4.

Abstract model and local view
The abstract model for highway traffic consists of neighbouring infinite lanes 0, 1, . . . of continuous space, leading in the same direction from the set of all lanes L. Every car has a unique car identifier A, B, . . . from the set I of all car identifiers and a real value for its position pos on a lane. An example for a traffic situation in our abstract model is depicted in Fig. 1. We use the concept of an ego car as the car under consideration and use the special variable ego to refer to this car. For Fig. 1, we assume E is our ego car and thus have the valuation ν(ego) = E.
In the abstract model, the space a car E is currently occupying on a lane is represented by its reservation res(ego), while a claim clm(ego) is akin to setting the direction indicator (cf. dotted part of cars A and B in Fig. 1, showing the desire of A and B to change to lane 1). Thus, a claim represents the space a car plans to drive on in the future. For now we assume, that the size of a car includes its' physical size and its braking distance. With this, safety is already violated, if a car invades the braking distance of another car. The idea is that every car is supposed to be able to do an emergency brake at every moment, without causing a collision.
Static information about cars like their positions and their reserved or claimed lanes is captured in a traffic snapshot TS = (res, clm, pos, spd, acc) from the set TS of all traffic snapshots. Note that we assume there exists a minimal positive value for the size of all cars, thus only finitely many cars are considered in a view. We furthermore assume that there exists a maximum velocity for all cars and the horizon h is big enough to consider the fastest car that could endanger E contained in its the standard view V (E, TS). In the example in Fig. 1, car D is not considered in V , as it is to far away from E.
We use a car dependent sensor function Ω E : I × TS → R + which, given a car identifier C ∈ I and a traffic snapshot TS ∈ TS, provides the size Ω E (C, TS) of C as perceived by E's sensors.
For a view V = (L, X, E) and a traffic snapshot TS = (res, clm, pos, spd, acc), we introduce the following abbreviations, used for the semantics definition of our logic MLSL in the next Sect. 2.2: The functions (1) and (2) restrict their counterparts res(C) and clm(C) from TS to the set of lanes considered in V . Function (3) defines the part of car C that E perceives with its sensors in the extension X of the considered view V .

Multi-lane Spatial Logic
With Multi-lane Spatial Logic (MLSL), we can reason about traffic situations in our local view V . As variables, we allow for car variables c, d, . . . from the set CVar, valuated with car identifiers from the set I and lane variables n, l, . . . from the set LVar, valuated with lanes from L. We define ego ∈ CVar.

Definition 2 (Valuation of variables).
A valuation ν is a function ν : Var → I ∪ L, where Var = CVar ∪ LVar and ν : CVar → I and ν : LVar → L. Formulae of MLSL are built from atoms, Boolean connectors and first-order quantifiers. As spatial atoms, we use free to represent free space on a lane and re(c) (resp. cl(c)) to formalise the reservation (resp. claim) of a car. We also allow for the comparison of variables u = v for variables u, v, ∈ Var of the same type.
We use a horizontal chop operator similar to chop operations for timing intervals in Duration Calculus [6] or interval temporal logic [21], denoted by . Also, we introduce a vertical chop operator given by the vertical arrangement of formulas. Intuitively, a formula ϕ 1 ϕ 2 holds if we can split the view V vertically into two views V 1 and V 2 such that on V 1 the formula ϕ 1 holds and V 2 satisfies ϕ 2 . Similarly a formula where c ∈ CVar and u, v ∈ Var. We denote the set of all MLSL formulas by Φ M .
The semantics of MLSL formulas is defined over a traffic snapshot TS, a view V and a valuation of variables ν. We denote the length of a real interval X ⊆ R by |X|. Definition 4 (Semantics of MLSL). The satisfaction of MLSL formulas ϕ with respect to a traffic snapshot TS, a view V = (L, X, E) with L = [l, n] and X = [r,t], and a valuation ν of variables is defined inductively as follows: TS,V, ν |= free ⇔ |L| = 1 and |X| > 0 and ∀i ∈ I V : len V (i) ∩ (r,t) = / 0 TS,V, ν |= re(c) ⇔ |L| = 1 and |X| > 0 and ν(c) ∈ I V and res V (ν(c)) = L and X = len V (ν(c)) TS,V, ν |= cl(c) ⇔ |L| = 1 and |X| > 0 and ν(c) ∈ I V and clm V (ν(c)) = L and X = len V (ν(c)) Abbreviation. In the following we use the abbreviation ϕ to state that a formula ϕ holds somewhere in the considered view. For example, in Fig. 1 with valuation ν(ego) = E, the formula ϕ ≡ re(ego) holds in V (E, Road), because there somewhere exists a reserved space for car E. Example 1 (MLSL formulas). Consider Fig. 1 and assume a valuation of variables ν(ego) = E, ν(a) = A, ν(b) = B and ν(d) = D. Consider the following MLSL formulas: In view V (E, TS) the formula ϕ 1 holds, as there is free space in front of car E. Equally ϕ 2 holds, as there is a claim of both cars A and B at the same spot on lane 1 and after this there is a space with only the claim of car B. Thus TS,V (E, TS), ν |= ϕ 1 and TS,V (E, TS), ν |= ϕ 2 . However, TS,V (E, TS), ν |= ϕ 3 , as car D is not part of view V (E, TS).

Automotive-controlling timed automata
Before we introduce the actual lane change controller protocol from [13] in Sect. 2.4, we briefly define the extended timed automata type, introduced in [14] to formalise the controller. As variables these automotive-controlling timed automata (ACTA) use both clock and data variables. For clock variables x, y ∈ X and clock updates we refer to the definition of timed automata [1] and for data variables u, v ∈ Var and data updates we refer to the extension of timed automata proposed for UPPAAL [9]. These clock and data updates ν act are allowed on transitions of ACTA.
Further on, the controllers use MLSL formulas ϕ M as well as clock and data constraints ϕ X resp. ϕ Var as guards ϕ on transitions and invariants I(q) in states q. An example for a data constraint for a variable l ∈ Var is l > 1. A guard or invariant ϕ from the set Φ of all guards and invariants is defined by We express possible driving manoeuvres by controller actions, which may occur at the transitions of an ACTA. Controller actions e.g. enable a car to set or withdraw (wd) a claim (c) or a reservation (r) for a lane.

Definition 5 (Controller Actions).
With c ∈ CVar, a controller action c act is defined by The set of all controller actions is defined by Ctrl Act .

Lane change controller
In this section, we introduce the lane change controller from [13], whose implementation into UPPAAL we introduce in Sect. 3. The overall goal of this controller is to safely change lanes in freeway traffic. Here, safety of ego car means collision freedom and thus disjunction of the reserved spaces of ego and other cars, expressed by the MLSL formula The main idea for the lane change controller is to first claim the space on a lane it wants to enter and reserve it only if no collision is detected. We assume a lane change to take at most t lc time to finish. The lane change controller is constructed for the ego car (ν(ego) = E in the example from Fig. 1) but scales to all cars as ego can be substituted by an arbitrary car variable c ∈ CVar.
We explain the construction of the controller starting with the initial state. As we want to prevent different reservations from overlapping, we introduce a collision check for the ego car expressed by the MLSL formula cc ≡ ¬∃c : c = ego ∧ re(ego) ∧ re(c) .
Formula (5) is evaluated to true, iff nowhere exists a car different from the ego car whose reservation overlaps with the actors reservation. We assume cc to hold in the initial state of our controller. Next the lane change controller can claim some space on either the lane to its left or right, provided such a lane exists. Here N is the lane identifier of the highest lane from the set of all lanes L.
In order to transform a claim into a reservation and thus finally change lanes, a car first needs to check if there are overlaps of other cars' claims or reservations with its own claim. This is formalised by the potential collision check Formula (6) evaluates to true, iff there exists a car different from the ego car whose claim or reservation overlaps with ego car's own claim. A (temporary) potential collision is allowed, because it does not endanger the safety property (4). However, if a potential collision is detected, the car must withdraw its claim immediately.
When ∃c : pc(c) does not hold, the actor reserves the claimed lane and starts changing lanes. To prevent deadlocks, we set a time bound t in state q 2 for the time that may pass between claiming and reserving crossing segments. After t lc time, the lane change is finished and the reservation of actor E is reduced to the new lane.

UPPAAL Implementation and Verification
We first introduce the specific abstract model we examine with UPPAAL and the considered assumptions and restrictions for it in Sect

Overall scenario and data structure
The model we examine with UPPAAL is the traffic situation depicted in Fig. 1, where we consider lanes 0 to 3 and the cars A, B and E contained in view V (E, TS). We encode the traffic snapshot TS, more precisely the positions, claims and reservations of the cars on the lanes, by a global data structure pos t. For reservations res this is encoded as follows:

Distance Controller
The lane change controller is not responsible for distance keeping. However, for cars with different acceleration and speed, a controller for distance keeping is inevitable to avoid rear-end collisions. Such a distance controller is outlined, but not formalised or constructed in [13]. Another possible distance controller is introduced and formally verified, but not yet implemented in [8]. Recently, the group of Kim Larsen synthesised an adaptive cruise control distance controller with the UPPAAL extension Stratego [15]. As the authors base their work on the spatial model of MLSL, this approach is of high interest for our implementation. However, they only consider a model consisting of one single lane without any neighbouring lanes and only two specific cars ego and f ront (cf. Fig. 3). Their idea is, that the ego car keeps track of its distance to the f ront car always. Additionally, their goal is to minimise the distance between ego and f ront. For this, one UPPAAL automaton for each ego and f ront is used, additional to a system controller.  Consider on the other hand our multi-lane scenario, e.g. in Fig. 4. It is not enough to keep track of the distance to f ront, as cars A, B, C and D might change lanes and thus be in front of ego any time. Thus, we also need to keep track of the distances to these cars. A problem here is state space explosion, as the number of considered parallel timed automata for UPPAAL increases significantly, when using the approach from [15] directly. A second problem is the discretisation of space in their approach.
Cars of interest for ego Figure 4: Cars of interest for ego car for distance keeping in multi-lane highway scenario [13].
However, for examining the safety and liveness solely of the lane change manoeuvres with the controller from [13], we do not need to consider a scenario with cars with different speed and acceleration. We restrict all cars to have the same constant speed whereby the relative distances between the cars along the lanes never change. Although this is a strong restriction, it is reasonable, as our goal is to show safety and liveness of lane change manoeuvres, where collision freedom while changing lanes is considered, not rear-end collisions.
Nonetheless, as a constant speed for all cars is a strong assumption, we plan to implement a version of the adaptive cruise controller from [15] in future work for a more realistic model.

Generic model
Despite the speed limitation, we encode a preferably general behaviour. In our model, the expected behaviour of car E is that it is always able to change lanes and that there can never occur a potential collision or collision with E, as there is no conflicting car on any neighbouring lane. In contrast, cars A and B can not always change lanes, as their position intervals [10,15] and [12,17] would intersect if the cars had reservations or claims on the same lane. Thus, we expect potential collisions between A and B, but show that the lane change controller always prevents actual collisions. r e t u r n e x i s t s ( l a n e : l a n e i d t ) p1 . l a n e [ l a n e ] and p2 . l a n e [ l a n e ]

Verification of Safety with UPPAAL
The requirement queries for the verifier in UPPAAL are formulated in a computation tree logic (CTL) [7,26] style specification language. The first query we successfully check is with which we globally exclude deadlocks in an arbitrary run of our system. We checked the query on a normal work station in 48 to 49 seconds with a memory usage peak of roughly 140KB. For the second query, we introduce the Observer automaton Observer1, depicted in Fig. 6. This Observer automaton uses a slightly adapted version of the collision check cc() to check for a collision between any two arbitrary cars at any moment. We use the query A[] not Observer1.unsafe (8) to show in averagely less than 4 seconds with a memory usage peak of 46KB, that there exists no example trace where the formula cc does not hold. With this query, we verify the safety property (4) (p. 21) for the lane change controller from [13].

Adaptions for constructing a live controller
With query (7), we exclude deadlocks in our system. However, the original controller in Fig. 1 is not truly live, as e.g. livelocks exist, where no car ever changes lanes, even though in our model at least car E, should always be able to change lanes.
To analyse liveness, we introduce a second Observer automaton Observer(i), as depicted in Fig. 7. For every instance LCP(i) of the lane change controller, we require an automaton Observer(i) which synchronises with LCP(i) over communication channels. E.g. on claiming a lane for car A, LCP(A) sends over the channel claiming[A] with which Observer(A) synchronises, such that both controllers simultaneously change to a new state. Upon reserving a lane, LCP(A) sends over reserving[A] and the Observer changes to a state success. We check the query A<> (Observer(A).success or Observer(B).success or Observer(E).success), (9) which states, that finally in every trace, at least one of the controllers LCP(i) is successful in changing a lane. Remember, that we generally expect query (9) to be successfully verified, as in our model at least car C should be able to finally change a lane in every possible trace.

Adaption 1
Without a time invariant in state q 1 of the original controller from [13] and without respective time guards on the outgoing edges, query (9) does not hold.
The reason is that there exists a trace, where cars A and B both infinitely often claim lane 1 without any elapse of time and thus both circle between their respective states q 0 , q 1 and q 2 in a livelock. As no time elapses, LCP(E) has no possibility of executing any transition and thus starves. This problem is easily solvable by introducing the invariant x <= t w to state q 1 and placing the guard x >= t w on the outgoing edges of q 1 , as done in the UPPAAL automaton depicted in Fig. 5. With these adaptions, we successfully show query (9) in less than 0.5 seconds with a memory usage peak of 40KB.

Adaption 2
The verification query (9) is already a weak liveness property, as it shows that in every simulation trace, at least one of the controllers finally changes lanes. We refine this property to A<> Observer(i).success, which states for an arbitrary car identifier i, that the related car finally changes lanes. When considering only the first adaption, as anticipated, this property only holds for LCP(E). The reason is, that there still exists a trace, where cars A and B both unsuccessfully try to change to lane 1 infinitely often and thus creating a potential collision infinitely often, preventing both controllers from ever transforming their claim into a reservation.
To solve this, we introduce an additional state q_wait, in which the controller is forced to wait for a bounded non-deterministic time. For now, we delimit this waiting time in q_wait by its invariant x ≤ 4 and the guard x ≥ 1 on its outgoing edge. With this, cars A and B do not permanently block each other from changing a lane and we verify both A<> Observer(A).success and A<> Observer(B).success (11) in each less than 2.7 seconds with a memory usage of each less than 76KB.

Summary and extendability of the current implementation
With the traffic situation from Fig. 1 and the corresponding implementation, as described in this section, we presented one very specific scenario, designed for the following purposes: • Showing the absence of collisions between any cars (i.e. proving safety (4)) and • Identifying and analysing the existing livelocks (cf. location q 1 ) and • Eliminating the livelocks and showing liveness of the new controller.
For this, the restrictions for the scenario, e.g. on 3 cars and 4 lanes were reasonable. However, we also tried different scenarios, with different numbers of lanes and cars. Our liveness and safety properties were not violated for any of the considered numbers of lanes and cars. Up to 16 parallel lanes were considered without any problems. However, we observed the following run-time issues when adding cars. While run-time seemes to increase only linear by about 50 ms each time when we add one lane, it appears to increase exponentially when adding a car. This observation is not surprising, as adding only one car i means adding two timed automata and one clock variable to the system: One timed automaton LCP(i) with its clock x and one observer automaton Observer(i).
Consider for example the model from Fig. 1 with one additional car. Now for property (11), UPPAAL takes 1025 seconds to verify the query instead of the previously observed 2.7 seconds for the three car scenario. While 1025 seconds for four cars is still acceptable, after including a fifth car, UPPAAL could not finish the verification of query (11) within one day.
Thus, for future considerations of our implementation where more than four cars should be considered, we would have to optimise our implementation first.

Conclusion
We strengthened the MLSL approach from the group of Olderog [13,12,14], by implementing their lane change controller for highway traffic in UPPAAL and successfully verified their safety property. We additionally optimised their controller by examining and implementing liveness properties into it.

Related Work
There exist several approaches for analysis and control of traffic using intelligent transportation systems, where e.g. in [18] traffic lights are used as a central control mechanism at intersections. The authors verify safety of their hybrid systems with the tool KeYmaera. There also exists an approach to synthesise intelligent traffic light control mechanisms with the UPPAAL extension Stratego [3]. The key idea of this approach is to minimise waiting times and energy waste.
Also various approaches for safe and autonomously driving systems were implemented during the DARPA Grand Challenge, where e.g. finite state machines were used to describe the autonomous behaviour of the cars [25,28].
For a hazard warning extension of MLSL, a dedicated hazard warning controller was implemented in UPPAAL [24]. However, the hazard warning controller was focused on a timely warning message delivery via broadcast channels and did not use MLSL formulas. A combined proof of UPPAAL verification queries with a formal proof by induction was used to prove the timely warning delivery.

Future Work
In the end of Sect. 3.4, we observe that cars A and B block each other on lane 1 and suggest an adaption ensuring the liveness of the controllers. However, this adaption does not guarantee fairness, as one of the cars could get the right of changing lanes arbitrarily more often than the other car. To overcome this problem, we could implement a notion of fairness into LCP(i), where either car A or car B lets the other car go first, when they already got the right of way often enough. Also, we could use the UPPAAL extension for stochastical model checking (UPPAAL SMC) [4], to analyse the probabilities of unfair behaviour. We could add prices to the transitions of our controller, which increase, when a car unsuccessfully claims too often.
In this paper, we only considered the lane change controller for highway traffic [13]. An implementation of their lane change controller for country-roads [12] and the crossing controller for intersections [14] would be highly interesting. Also, they published results on a relaxation of their assumption of perfect knowledge, where the controllers communicate, to cope for the missing information. Also, for future considerations with more cars or different controllers, an optimisation of our implementation is of high interest, as described in Sect. 3.5.
Last but not least, for now we have the assumption of a constant speed. To verify properties in a more realistic scenario, our cars should be able to dynamically change their speed. To this end, we plan to implement an adaption of the existing UPPAAL Stratego distance controller from [15], as described in Sect. 3.1. Their adaptive cruise control implementation also minimises the distance between the ego car and the car in front, which we could use to optimise the traffic flow in our scenario. With this, we could even extend our MLSL scenario to a platooning scenario (cf. PATH Project [19] and the European SARTRE project [5]). However, as outlined in Sect. 3.1, the adaption of the distance controller from [15] poses some non-trivial challenges.