The degree of automation in our daily life will grow rapidly. This leads to big challenges regarding the safety validation of autonomous robots which take over more and more tasks being { as of yet { predestinated for humans. This is in particular true for the emerging area of autonomous driving which aims at making road tra c safer, more e cient, more economic, and more comfortable. One promising approach for the safety validation of autonomous driving is the virtual simulation of tra c scenarios, i.e. conducting the majority of tests in virtual reality instead of the real world. In addition to quantity, the quality of such tests with a focus on critical tra c scenarios will be an essential ingredient for safety validation. In this paper, we investigate the concretization of tra c scenarios { in particular, scenarios which are speci ed as a set of constraints with interval parameters. We rely on the iSAT algorithm to perform the core reasoning, adapt its decision heuristics and complement it with an ICP-aware formula generation for non-linear formulas. The resulting Scenario Concretization Solver (SCS) { although being written in Java { is able to outperform SMT solvers on this problem class.
Virtual safety validation is bound to play an increasingly important role in the development of complex systems.
This is especially true in the context of autonomous driving { where achieving a convincing degree of coverage
purely by testing an autonomous vehicle in the real world may not only be impractical (cf. e.g. [
The need for virtual validation has thus been widely recognized in both industry and academia [
An essential element in the virtual validation of autonomous vehicles is subjecting the so-called \ego vehicle" (i.e. the vehicle to be tested) to various tra c scenarios that describe real-world situations. Such tra c scenarios can be written manually by experts (e.g. requirement engineers, tra c experts, even by function developers who are keen on getting quick feedback), can be derived from past experience of critical situations (e.g. accident data bases), or by observing real-world tra c. In either case, a scenario may have to be designed or to be analyzed by human operators, who need to have a quick grasp of the contents of the scenario. At the same time, scenarios need to have a clear semantics to allow unambiguous communication, simulation, and testing.
This important topic of scenario formalization is still the subject of ongoing e orts to develop and
standardize scenario formats in academia, e.g. tra c sequence charts [
In our view, scenarios need to accommodate di erent levels of abstraction to allow for an e cient use of modeling e ort. By specifying a scenario on an abstract level and using partially or fully automated variation strategies, one abstract scenario can lead to a huge number of concrete test cases. One essential element by which this degree of abstractness can be controlled is the use of intervals for the description of e.g. velocities, distances, and speed di erences. Using relatively large intervals within a scenario leads to a wide range of possible executions and may thus lower the e ort needed to write more speci c concrete instances of the scenario manually.
Within this paper, we present a solver for the (discrete-time) concretization of abstract scenarios. There are in fact multiple purposes of such a concretization. Firstly, scenario concretization allows the modeler of a scenario to check the plausibility and validity of the scenario by seeing one or even multiple concrete instances of it. Unintended behavior can thus be detected as well as inconsistencies be analyzed and xed. Secondly, a concretization may help to actually execute the scenario during simulation. While a concretization in the form of trajectories for all involved vehicles cannot be used directly as a test case (since the ego vehicle as system under test must of course be allowed to behave freely during the test), the concretization may be used to nd a dynamic or rather reactive test strategy that adapts the surrounding vehicles to the ego vehicle's behavior. Thirdly, scenario concretizations can be in uenced by adding side constraints that describe di erent regions of the solution space. Scenario concretization may thus be used as a form of guided scenario variation { a part of the possible automation that reduces the manual e ort needed to specify scenarios. 2 A tra c scenario is de ned by the following elements. Let IR denote the set of closed intervals over the real numbers R including the (half-)open intervals containing 1 and +1. We further denote by ID a unique identi er. For the sake of simplicity, we restrict the scenarios to the two dimensional plane and a straight road (both limitations could be lifted at a later stage). We call x the longitudinal direction parallel to the direction of the road and y the lateral direction orthogonal to the road.
Vehicle Type: A vehicle type consists of ranges for speed [vmin; vmax] 2 IR and acceleration [amin; amax] 2 IR.
Lane: A lane is de ned by an ID, a width w 2 R, and a left and right neighboring lane, which may or may not exist.
1https://www.asam.net/standards/detail/openscenario/ Lane Constraint: A lane constraint, denoted by lane(h; s; t; r), is de ned by a vehicle h, a source lane s, a target lane t, and a change rate r 2 IR.
Distance Constraint: A distance constraint is de ned by two vehicles h1 and h2, an initial distance i 2 IR, an invariant distance d 2 IR, a nal distance f 2 IR, and a distance change rate r 2 IR. It is denoted by distance(h1; h2; i; d; f; r). All distances are given only with respect to the x dimension, such that e.g. two cars driving alongside on di erent lanes, would have a distance of 0. It should be noted that the invariant distance d is only partially handled by the current SCS version (cf. Section 3.3).
Speed Constraint: A speed constraint, denoted by speed(h; i; s; f; r), is de ned by a vehicle h, an initial speed i 2 IR, an invariant speed s 2 IR, a nal speed f 2 IR, and a speed change rate r 2 IR. This speed is given only with respect to the x dimension, i.e. the lateral component during lane changes is ignored. Speed Di erence Constraint: A speed di erence constraint is de ned by two vehicles h1 and h2, an initial speed di erence i 2 IR, an invariant speed di erence s 2 IR, a nal speed di erence f 2 IR, and a speed di erence change rate r 2 IR. It is denoted by speed di (h1; h2; i; s; f; r). Also in this case, only the velocities in the x dimension are considered.
c Phase: A tra c phase P = (d; L; H; e; C) is given by an admissible duration d 2 IR, a set L of lanes, a set H of vehicles with one prominently labeled as \ego vehicle" e 2 H, and a set C of lane, distance, speed, and speed di erence constraints de ning the initial, invariant, and nal states admissible within that phase.
c Scenario: A tra c scenario S = (P1; : : : ; Pn) is given by a sequence of tra c phases P1, : : :, Pn with the same ego vehicle e in each phase, i.e. e = ei for each ego vehicle ei of Pi. 2.2
The semantics of a tra c scenario S is given by runs. Intuitively, a run comprises the behavior of all vehicles of the tra c scenario that match all the constraints of the tra c phases. The model of the physical behavior of a vehicle for a step of (arbitrary) duration t 2 R is given by the following equations, with x, y, vx, vy, ax, ay being the x and y position as well as the speed and acceleration in x and y directions, respectively. The primed version w0 of a variable w denotes the value of w after the step.
vx0 = vx + vy0 = vy + x0 = x + y0 = y + t ax t ay t 1=2 (vx0 + vx) t 1=2 (vy0 + vy) (1) (2) (3) (4) For a vehicle h let s(h) be some valuation for all state components x, y, vx, vy, ax, ay of v. For a vehicle h and a lane, distance, speed, or speed di erence constraint c, we de ne init(s(h); c), inv(s(h); c), and nal(s(h); c) to be true if and only if the initial, invariant, and nal constraints of c, respectively, are satis ed by valuation s(h). Run of a Tra c Scenario: Let S = (P1; : : : ; Pn) be a tra c scenario with Pi = (di; Li; Hi; ei; Ci) being a tra c phase. A run
r = ((t11; s11); : : : ; (t1m1 ; s1m1 ); : : : ; (t1n; s1n); : : : ; (tnmn ; snmn )) of S satis es the following conditions with tij 2 R being increasing time points and sij (h) for all h 2 Hi being a valuation for all state components of h.
All vehicles follow the model of the physical behavior described by equations 1, 2, 3, and 4, i.e. for r = (: : : ; (t; s); (t0; s0); : : :), we have t = t0 t and s0 and s are connected by equations 1, 2, 3, and 4.
81 i n : timi ti1 2 di.
The initial constraints of the rst phase P1 are satis ed: 8h 2 H1 8c 2 C1 : init(s11(h); c).
The initial constraints of each phase Pi>1 are satis ed: 81 < i n 8h 2 Hi 8c 2 Ci : init(simi1 1 (h); c).
The invariant constraints of each phase are satis ed: 81 i n 81 j mi 8h 2 Hi 8c 2 Ci : inv(sij (h); c).
The nal constraints of each phase satis ed: 81 i n 8h 2 Hi 8c 2 Ci : nal(simi (h); c). In our formalism, a simple overtaking scenario with two vehicles h1 and h2 could be modeled in three phases as follows. While h2 stays on the right lane in all phases, h1 changes from the right to the left lane in the rst phase, stays on the left lane in the second phase and changes back to the right lane in the third phase. Additionally, the distance between both vehicles changes. While being behind h2 in the rst phase, h1 overtakes h2 in the second phase and stays in front of h2 in the third phase. In all phases h1 has at least the same speed as h2, i.e. the speed di erence between both vehicles is less than or equal to zero. Or more formally: Let T be a vehicle type with v 2 [ 5:5; 69] and a 2 [ 10; 5:5].
Let h1 and h2 be two vehicles of type T and let H = fh1; h2g.
Let left and right be two neighboring lanes and let L = fleft; rightg.
Let c1; c2; : : : ; c12 be constraints and let denote the interval (
1; +1): = distance(h1; h2; ; [4; 10]; [2; 5]; ) = speed di (h1; h2; ; ( 1; 0]; ; ) = lane(h1; right; left; [0; +1)) = lane(h2; right; right; [0; 0]) = distance(h1; h2; [2; 5]; ; [ 5; 2]; ) = speed di (h1; h2; ; ( 1; 0]; ; ) = lane(h1; left; left; [0; 0)) = lane(h2; right; right; [0; 0]) = distance(h1; h2; [ 5; 2]; ( 1; 2]; ; ) = speed di (h1; h2; ; ( 1; 0]; ; ) = lane(h1; left; right; ( 1; 0]) = lane(h2; right; right; [0; 0]) Let C1 = fc1; : : : ; c4g, C2 = fc5; : : : ; c8g and C3 = fc9; : : : ; c12g.
Let Pi([1; 5]; L; H; h1; Ci) with i 2 f1; 2; 3g be three tra c phases.
Then SA = (P1; P2; P3) is a simple overtaking scenario.
In Section 4 this scenario is parameterized by the number of vehicles and phases. Similar to h2, every additional vehicle stays on the right lane in all phases. Furthermore, distance constraints are added to ensure that hi+1 drives in front of hi for i 2. Another variant of SA (denoted SB) is obtained by introducing additional speed di erence constraints. If the number of phases is increased, extra overtaking maneuvers are performed until there is no further vehicle to overtake { in this case h1 stays in front of the last vehicle hn for the remaining phases. 3
As explained in the previous section, our scenario formalism uses intervals to constrain the behavior of the vehicles. For example, a vehicle h might be required to have a speed between 20 m/s and 25 m/s at the beginning of a phase { i.e. c1 = speed(h; i; s; f; r) with i 2 [20; 25]. Thus, it is only consequent to check whether the intervals within a constraint are consistent. For example, if c1 additionally constrains the invariant speed s to [27; 30], then this contradicts with the initial speed i { as the interval of i does not intersect with the interval of s. On the other hand, in case i and s have an intersection (e.g. with i 2 [20; 25] and s 2 [23; 30]), then it is possible to con ne i to [23; 25].
Unfortunately, such a simple interval intersection check only covers some of the dependencies within a
constraint. Furthermore, such a check is unable to handle dependencies between di erent constraints. For example,
let vehicle h1 have an invariant speed interval of [20; 25] while vehicle h2 has an invariant speed interval of [27; 30].
Additionally, let h1 and h2 be at di erent lanes but at the same longitudinal position at the beginning of a phase
P. Obviously, the distance between h1 and h2 is zero at the beginning of P but will increase over time { as h2
is strictly faster than h1. Hence, there could be a con ict with a distance constraint depending on the allowed
duration of P. Similar to the equations for the physical behavior of a vehicle (cf. Section 2.2), the dependencies
between the speeds of h1 and h2, their distance and the phase duration can be expressed symbolically in a
formula (cf. Section 3.3). As the involved variables have interval valuations, Interval Constraint Propagation
(ICP) [
Our approach builds on ICP { but embeds it into the Con ict-Driven Clause Learning (CDCL) [
In order to keep the paper self-contained we start with a short and informal introduction to ICP, before giving an overview of the iSAT algorithm. The nal two subsections contain the main contributions of this paper: the ICP-aware conversion from a given constraint set to a formula as well as the heuristics which selects a variable for the next interval split to be performed. 3.1
When considering an equation like x = y + z, the variables x, y and z are usually understood as placeholders
which stand for single values. This is generalized when performing ICP [
If an equation contains more than one arithmetic operation, it is possible to build a dedicated interval
propagator for it. Alternatively and similar to the Tseitin-transformation [
As described, each equation and its redirected forms are handled individually by ICP. An equation x = y z with 2 f ; +; ; =g is consistent regarding the interval valuation of its three variables, if the intervals of x and y z have a non-empty intersection. If an equation is consistent, then it is guaranteed to have a solution within the intervals of the variables contained in the equation. But there is no such guarantee if ICP is applied to a conjunction of multiple equations, i.e. the consistency of all equations does not imply the existence of a solution. For example, in the case of x = y + z with x 2 [0; 0] and y; z 2 [ 10; 10] there is a dependency between y and z. On the one hand, for each y 2 [ 10; 10] there is a z 2 [ 10; 10] such that y + z 2 [0; 0]. Thus, ICP cannot con ne the intervals of y and z. On the other hand, not every pair of values in the interval of y and z is a solution for x = y + z when x 2 [0; 0]. Hence, as the intervals of y and z stay unchanged, the dependency between both variables induced by the interval of x is not visible for ICP when examining w = y z with w 2 [0; 0]. The conjunction of both equations implies y = z = 0, but ICP is unable to detect this2. In a similar setting a set of further equations might imply other values for y and z, but as ICP keeps y; z 2 [ 10; 10] this inconsistency will stay undetected. Thus, when multiple equations are involved, the intervals determined by ICP overapproximate the set of solutions. In other words, if ICP detects an inconsistency there is indeed no solution { in case all equations are consistent, the current interval valuation of all variables might or might not contain a solution. Therefore, a further mechanism is needed to obtain a method which is able to nd a solution or prove the absence thereof.
The basic idea to get such a method is to reduce the width of the intervals. If, in the extreme case, all variables have point intervals (i.e. an interval width of zero and thus single values), then the consistency of all equations proves that the current valuation is a valid solution. Hence, intuitively, if all equations are consistent and the interval widths of all variables are very small, one could call this an almost-solution. This directly relates to the robustness mentioned earlier. If small perturbations are allowed (i.e. by adding a small individual perturbation constant to each equation), then this almost-solution can be used to obtain a valid solution for such a perturbed conjunction of equations { e.g. by (a) taking the midpoint of each interval, and (b) calculating the needed perturbation constant for each equation. Hence, the question remains how to reduce the width of the intervals.
This can be achieved by performing heuristic decisions in the form of interval splits. For example, the midpoint of an interval could be chosen as the new upper or lower bound. This is repeated until all intervals have a width below a given minimum splitting width. After performing such an interval split, ICP is applied again to deduce the consequences of the split. Of course, such a heuristic decision might lead to an inconsistency. In such a case, the last decision has to be reverted in order to try the interval part which was excluded by the split { resulting in a search process with backtracking. Instead of just reverting the last decision, it is also possible to perform a more thorough analysis to isolate the cause of the current inconsistency { which is not necessarily the last decision. Such an analysis is part of the iSAT algorithm. Its details are explained in the next subsection. 3.2
In order to perform a more thorough analysis in case of an inconsistency, an implication graph is used to keep track of the deductions performed by ICP. Besides the deduced lower or upper bounds, it also contains the reasons for each deduction { i.e. the relevant bounds of the other variables in the equation examined by ICP. For example, if ICP examines the equation x = y + z together with the current interval valuation x 2 [0; 10], y 2 [2; 5] and z 2 [1; 3], then the newly deduced lower bound of x is recorded as ((y 2) ^ (z 1)) ) (x 3) in the implication graph. Thus, (y 2) and (z 1) can be understood as the reasons for this deduction.
The implication graph is partitioned into decision levels { one level for each decision (i.e. a heuristic interval
split). If ICP detects an inconsistency, then an interval of a variable x became empty, i.e. xlb > xub. If this
inconsistency happens on decision level 0 (i.e. without performing a decision), the formula is proved to have no
solution { i.e. it is unsatis able and no further analysis is required. Otherwise, xlb and xub are analyzed { as
at least one of both bounds was deduced by ICP and thus has reasons. Basically, those reasons which were
themselves deduced on the current decision level are analyzed in order to obtain one reason which is the rst
unique implication point (1UIP) [
2In this concrete case the e ect can be mitigated by adding: (y2 = 2 y) ^ (z2 = 2 z) ^ (w = x y2) ^ (w = z2 x)
Here, we motivated the iSAT algorithm as ICP-based search process with non-chronological backtracking and
learning. In the context of satis ability checking, the motivation is somewhat di erent. Satis ability Modulo
Theories (SMT) considers Boolean combinations of theory atoms { e.g. Boolean combinations of equations and
inequalities containing non-linear real arithmetic. When performing lazy SMT solving, the Boolean skeleton is
processed by a (usually CDCL-based) SAT solver which determines a valuation for the truth values of the theory
atoms. A separate theory solver is used to check whether there is a solution in the conjunction of theory atoms
under the given truth values. If this is not the case, a (hopefully) small subset of the theory atoms is returned as
con ict explanation to the SAT solver. In the iSAT algorithm there is no separation between the SAT solver and
the theory part { instead ICP is tightly integrated into CDCL. In fact, each interval bound can be considered
as a literal { depending on its polarity it represents a lower or an upper bound. Thus, the iSAT algorithm
performs CDCL [
Our approach uses a solver core being similar to iSAT3 [
In the following we give an overview of the basic building blocks the complete formula is composed of. The current version of SCS divides each tra c phase into two sub-phases with equal duration3 { i.e. if di is the duration of Pi, then each sub-phase has duration d0i = 1=2 di. But in order to simplify the presentation of the formulas, we neglect this division. In fact, the formulas presented below are also used within a sub-phase { but depending on whether the sub-phase is the rst or last, the intervals speci ed by the constraints are applied to di erent variables, i.e. initial conditions are applied to the rst sub-phase, while nal conditions are applied to the last sub-phase.
As the duration di of a phase Pi might be an interval, it is a variable within the equations. Thus, the resulting set of equations is non-linear. For each vehicle h and each phase the following set of equations is generated for the x and y dimension (indices for h, x, y and the phase are omitted in favor of better readability): sum of speed average speed change of speed change of speed change of position change of position = = = = = = initial speed + nal speed 1=2 sum of speed
nal speed initial speed rate of speed di
nal position average speed initial position di In case of the y dimension initial position and nal position are point intervals representing the center of the source lane s and target lane t speci ed in the lane(h; s; t; r) constraint. The change rate r from this constraint corresponds to the invariant speed in the y dimension. As shown in Section 2.2, the speed evolves linearly from its initial to its nal value within each time step. Thus, it su ces to use the interval of the invariant speed as a further restriction for the intervals of initial speed and nal speed. For the x dimension, the position stays unconstrained while initial speed, nal speed and rate of speed are constrained by i, f and r from the speed(h; i; s; f; r) constraint. Here again, the invariant speed s is an additional restriction for initial speed and nal speed.
In case a distance() or speed di () constraint exists for a vehicle pair (h1; h2) in at least one phase, then the following set of equations will be added to each phase (the indices 1 and 2 correspond to h1 and h2 respectively): initial speed di
nal speed di change of speed di change of speed di change of speed di = = = = = initial speed2 nal speed2 nal speed di change of speed2 rate of speed di initial speed1 nal speed1 initial speed di change of speed1 di 3In the future we plan to determine the number of the sub-phases dynamically { e.g. depending on the phase duration sum of speed di average speed di average speed di initial distance
nal distance change of distance change of distance change of distance = initial speed di + nal speed di = 1=2 sum of speed di = average speed2 average speed1 = initial position2 initial position1 = nal position2 nal position1 = nal distance initial distance = change of position2 change of position1 = average speed di di It should be noted that these equations are only added for the x dimension { as the speed difference and distance are not considered in the y dimension. Each speed di (h1; h2; i; s; f; r) constraint restricts initial speed di , nal speed di and rate of speed di with i, f and r. The invariant speed di erence s is an additional restriction for initial speed di and nal speed di { similar to the speed() constraint. Furthermore, each distance(h1; h2; i; d; f; r) constraint restricts initial distance and nal distance with i and f as well as d. The change rate r restricts the invariant speed di erence and thus initial speed di and nal speed di . In contrast to the speed, the distance does not necessarily evolve linearly within a phase. In particular, it could happen that the distance reaches its peak somewhere within a phase { depending on how the speed di erence evolves. Hence, the invariant distance is only partially handled at the moment.
The formula creation is ICP-aware, i.e. it includes some redundant equations, which support the deductions performed by ICP. For example, it is advantageous to generate the above shown set of equations for a vehicle pair (h1; h2) in each phase { as this allows ICP to propagate the distances and speed di erences to the surrounding phases which might be subject to further constraints for this vehicle pair. Additionally, cyclic dependencies of vehicle pair constraints result in further equations to be added. For example, if the vehicle pairs (h1; h2), (h2; h3) and (h1; h3) are subject of distance or speed di erence constraints, then the following equations are generated: initial distance1;3
nal distance1;3 initial speed di 1;3 nal speed di 1;3 = = = = initial distance1;2 + initial distance2;3
nal distance1;2 + nal distance2;3 initial speed di 1;2 + initial speed di 2;3
nal speed di 1;2 + nal speed di 2;3 3.4
Due to the formula structure and the deductions performed by ICP, reductions in the interval width of the variables representing speeds or durations imply that the intervals of other variables will shrink as well, e.g. change of speed, average speed, change of position, change of speed di , average speed di as well as change of distance. Thus, intuitively, it seems to be advantageous to split speed and duration variables rst { this also conforms with our empirical observation. Therefore, we use three buckets for variables representing (B1) speeds or durations, (B2) distances, and (B3) positions. Variables in (B2) are only considered if (B1) is empty { similarly, all variables in (B2) are split before any variable from (B3) is processed. The variables in each bucket are selected pseudo-randomly. Furthermore, each interval split of a variable alternates between cutting o the lower or upper interval part { the size of this part varies pseudo-randomly between 1=3 and 1=8. Additionally, we use di erent minimum splitting widths in each bucket: (B1) 2 38, (B2) 2 37, and (B3) 2 36. 4
For technical reasons SCS is embedded into a Java-based framework and is itself written in Java4. As mentioned,
the core of SCS is similar to the core of iSAT3 [
R / #V / #P
SA UNS / 4 / 1 SA UNS / 4 / 2 SA UNS / 4 / 5 SA UNS / 4 / 10 SA UNS / 4 / 20 SB UNS / 5 / 1 SB UNS / 5 / 2 SB UNS / 5 / 5 SB UNS / 5 / 10 SB UNS / 5 / 20 SA SAT / 2 / 1 SA SAT / 2 / 2 SA SAT / 2 / 5 SA SAT / 2 / 10 SA SAT / 2 / 20 SA SAT / 3 / 1 SA SAT / 3 / 2 SA SAT / 3 / 5 SA SAT / 3 / 10 SA SAT / 3 / 20 SA SAT / 4 / 1 SA SAT / 4 / 2 SA SAT / 4 / 5 SA SAT / 4 / 10 SA SAT / 4 / 20 SB SAT / 3 / 1 SB SAT / 3 / 2 SB SAT / 3 / 5 SB SAT / 3 / 10 SB SAT / 3 / 20 SB SAT / 4 / 1 SB SAT / 4 / 2 SB SAT / 4 / 5 SB SAT / 4 / 10 SB SAT / 4 / 20 SB SAT / 5 / 1 SB SAT / 5 / 2 SB SAT / 5 / 5 SB SAT / 5 / 10 SB SAT / 5 / 20 P UNS solved P SAT solved
The comparison is performed on the basis of the formulas generated by SCS, i.e. the formulas are written out and converted to the HYS format (for iSAT3) and to the SMT2 format (for MathSAT, Yices, Z3 and CVC4)7. Thus, all solvers operate on the same formulas. In order to obtain small and large instances, the scenarios SA and SB (cf. Section 2.3) are parameterized regarding the number of vehicles and phases. The formula sizes range from 150 variables and 180 equations (containing arithmetic operations) up to 11 600 variables and 16 100 equations. We generated satis able and unsatis able instances { for an equal number of vehicles and phases the satis able and unsatis able instances only di er in the intervals constraining the variables.
The results are listed in Table 1. While the rst column shows the scenario family, the second column lists the expected result { i.e. whether an instance is satis able (SAT) or unsatis able (UNS) { as well as the number of vehicles and phases. The remaining columns either list the runtime in seconds or contain TO (for time-out) or MO (for memory-out). While the measurements for MathSAT, Yices, Z3, CVC4 and iSAT3 were performed under Debian 9 on an Intel Xeon E5-2690 with 2.6 GHz and a time limit of 900 seconds as well as a memory limit of 15 GB, SCS was executed under Windows 7 on an Intel Xeon E5-2695 with 2.3 GHz and a memory limit of 2 GB. Besides being written in Java and executed on a slightly slower CPU, the runtime of SCS contains an additional overhead of several hundred milliseconds: the import of the scenario from the surrounding framework, the creation of a trajectory for each vehicle to be visualized graphically as well as the generated formula being written to a le.
The results show that the unsatis able instances are solved within seconds in most of the cases. While MathSAT, Z3 as well as CVC4 have one unsolved instance, Yices, iSAT3 and SCS are able to solve all unsatis able instances. In case of iSAT3 the result is not surprising, because it applies the same ICP-based reasoning as SCS. With ICP the unsatis ability of the instances can be determined with a low number of non-chronological backtracking operations { the decision heuristics plays a minor role in these cases.
The picture changes when considering the satis able instances. Here, CVC4 and MathSAT each solve less than a third of the 30 instances. In particular, the instances of SA are hard to solve for both solvers. Yices and Z3 show better performance, but still have time-outs for 13 and 7 instances respectively. The numbers of iSAT3a, iSAT3b and SCS can be seen as an indicator for the e ectiveness of the decision heuristics used by SCS. As the the core of SCS is similar to the core of iSAT3, the numbers of iSAT3a give an impression how SCS would perform without its tailored decision heuristics. Although iSAT3b has only one time-out, the quality of its result (in terms of the margin a constraint might be violated) is worse compared to iSAT3a and SCS { in this set of instances, the violation margin of SCS is below 10 12, while it is above 10 3 for iSAT3b. This comes due to the coarser minimum splitting width used by iSAT3b. Additionally, it can be observed that iSAT3a exceeded its memory limit of 15 GB in four cases, while SCS stays within its limit of 2 GB for all instances. Hence, the decision heuristics of SCS prevents that ICP deduces millions of new bounds even with a very small minimum splitting width. Overall, SCS is the only solver which was able to solve all instances. Furthermore, its decision heuristics allows SCS to outperform the other solvers in particular on larger satis able instances. 5
In the context of safety validation for autonomous vehicles, virtual validation is one promising approach to reduce the amount of testing in the real world. In this context, formally speci ed scenarios are used to describe the real-world tra c situations which have to be tested. In order to derive a test case from such a scenario, a concretization is needed. In this paper we investigated the concretization regarding a constraint-based scenario formalism containing interval parameters.
We identi ed this problem class as another application of the iSAT algorithm. Exploiting the domain speci c knowledge, we adapted the solving strategy by an ICP-aware formula generation and a tailored decision heuristics. The resulting Scenario Concretization Solver (SCS) outperforms other solvers in particular on larger satis able instances. 7 http://www.btc-es.de/media/downloads/btc-es sc2 tra c scenarios.tar.gz