1 Introduction
Reactive synthesis is an automated process for deriving correct-by-construction reactive systems from temporal specifications [41]. Unlike traditional approaches that involve manual system construction followed by model checking, synthesis directly generates an implementation guaranteed to satisfy the given specification, provided such an implementation exists.
We focus on GR(1) [9], a fragment of Linear Temporal Logic (LTL). GR(1) specifications comprise initial, safety, and justice assumptions and guarantees. Initial properties define the expected state at the outset, safety properties specify invariants for all states and transitions, and justice properties describe conditions that must be satisfied infinitely often in any infinite run. GR(1) has gained popularity and was implemented in several tools, e.g., RATSY [6], Slugs [17], and Spectra [32], thanks to its relatively efficient symbolic synthesis algorithm and expressive power, capable of representing almost all of the common specification patterns identified by Dwyer et al. [16, 29]. Its balance of expressiveness and computational efficiency makes it suitable for a wide range of applications of reactive synthesis, e.g., in robotics [26, 30].
Anzeige
In this paper, we present a set of novel heuristics designed to improve the performance of GR(1) realizability checking and related algorithms. Developing specifications is a long, iterative process, just like developing program code. Our focus is on reducing the computational cost of the actual algorithms used in specification development to improve the developer experience.
We start by making the following high-level observations:
-
Many analyses used during specification development do not require the intermediate results of the GR(1) algorithm’s fixed-point iterations. These are required only for controller construction, but not for analyses such as realizability checking, non-well-separation detection [25, 31], inherent vacuity detection [34], and kind-realizability checking [22, 28].
-
The syntax of the specification, as written by developers, provides opportunities for deeper insight into the inner structure of the GR(1) game model and corresponding opportunities for performance improvements.
-
High-level language constructs simplify writing and reading complex specifications but often introduce hidden costs, such as additional variables and constraints. Some of these may be unavoidable, but others may be redundant.
Based on these observations, we present concrete heuristics that target various aspects of GR(1) realizability checking and related analyses:
-
A partial memoryless heuristics, which discards the parts of the memory accumulated during realizability checking that are not required for realizability checking and for previously presented heuristics from [19].
-
Heuristics to set an initial order on the variables of the specification and an order on the specification’s justice constraints, by embedding semantic information from the specification in a graph-based representation and using off-the-shelf graph algorithms to minimize graph bandwidth and compute the relative importance of nodes.
-
Heuristics to improve the embedding of finite automata into GR(1), to enable more efficient addition of high-level constructs like patterns and triggers.
All the heuristics we present are conservatively sound, that is, they never change the analysis result (except for one case, see Rem. 1). They only affect the computation’s total memory and time. Moreover, all the heuristics we present are fully automatic and completely transparent to the developer who wrote the specification.
Anzeige
We have implemented our ideas on top of the Spectra GR(1) synthesizer [32]. We chose Spectra due to its support for GR(1) and related algorithms, its use of existing heuristics [19], and the thousands of specifications it offers for extensive evaluation. Additionally, Spectra’s rich specification language includes high-level constructs such as counters, patterns [29], and triggers [5], allowing more expressive and readable specifications within GR(1).
We have validated and evaluated the implemented heuristics on benchmarks from the literature, including 3390 specifications from the SYNTECH benchmarks. Our results show major performance gains, in particular, an average of realizability checking at least two times faster than the baseline.
2 Background on GR(1) and Spectra
We provide a short background on GR(1) and Spectra, with references to relevant papers for more details and complete formal definitions.
2.1 GR(1)
Since LTL synthesis is computationally expensive (2EXPTIME-complete [41]), authors have suggested LTL fragments with more efficient synthesis algorithms, for example, GR(1) [9, 40], whose expressive power covers most of the well-known LTL specification patterns [16, 29]. GR(1) specifications include assumptions and guarantees about what needs to hold on all initial states, on all states and transitions (safety), and infinitely often on every run (justice). A GR(1) synthesis problem consists of the following elements [9]:GR(1) Realizability A GR(1) synthesis problem is strictly realizable iff the following LTL formula is realizable:GR(1) realizability can be checked using the 3-nested fixed-point algorithm shown in Alg. 1.
-
\(\mathcal {X}\) is a set of input variables controlled by the environment;
-
\(\mathcal {Y}\) is a set of output variables controlled by the system;
-
\(\theta ^e\) is an assertion, i.e., a propositional logic formula, over \(\mathcal {X}\) characterizing initial environment states;
-
\(\theta ^s\) is an assertion over \(\mathcal {V} = \mathcal {X} \cup \mathcal {Y}\) characterizing initial system states;
-
\(\rho ^e\) is an assertion over \(\mathcal V\cup \mathcal X'\), with \(\mathcal {X}'\) a primed copy of variables \(\mathcal {X}\); given a state, \(\rho ^e\) restricts the next input;
-
\(\rho ^s\) is an assertion over \(\mathcal V\cup \mathcal V'\), with \(\mathcal {V}'\) a primed copy of variables \(\mathcal {V}\); given a state and input, \(\rho ^s\) restricts the next output;
-
\(J^e_{i \in 1..n}\) is a set of assertions over \(\mathcal {V}\) for the environment to satisfy infinitely often (called justice assumptions);
-
\(J^s_{j \in 1..m}\) is a set of assertions over \(\mathcal {V}\) for the system to satisfy infinitely often (called justice guarantees).
$$\begin{aligned} \begin{aligned} \phi _{sr} = &(\theta _e \rightarrow \theta _s) \wedge (\theta _e \rightarrow G((H\rho _e) \rightarrow \rho _s)) \\ &\wedge (\theta _e \wedge G\rho _e \rightarrow (\bigwedge _{i=1}^n GFJ^e_i \rightarrow \bigwedge _{j=1}^m GFJ^s_j)) \end{aligned} \end{aligned}$$
(1)
2.2 Spectra
Spectra [32] is a specification language and a synthesis environment that includes a GR(1) synthesizer. It extends GR(1)’s Boolean variables to finite-type variables, e.g., enumerations and bounded integers. Beyond GR(1) with several performance heuristics [19], it includes extensions that are reduced into GR(1), e.g., patterns [29] and triggers [5], and comes with several analyses, e.g., well-separation detection [31] and repairs for unrealizable specifications [33]. Since 2015, Spectra has been used by hundreds of final-year CS undergrads in semester-long project classes at Tel Aviv University, specifying and executing robotic and other systems, resulting in the SYNTECH collection of specifications. Spectra is available from https://github.com/spectrasynthesizer.
Patterns and Triggers Dwyer et al. [16] have identified 55 LTL specification patterns considered common in industrial specifications. An example of a pattern is the property “p becomes true between q and r". Based on [29], a library of almost all of these 55 patterns has been added to Spectra by translating each pattern into a Büchi automaton and then using auxiliary variables, initial, safety, and justice constraints to embed it within the GR(1) specification.
Triggers are another Spectra language construct that aims to improve expressiveness and readability. Spectra triggers are similar to PSL triggers [18, 23]. A trigger is a formula of the form \(regexp1\ \mathtt {|=>}\ regexp2\), where regexp1 and regexp2 are regular expressions (REs) over assertions on the specification’s variables. regexp1 is the prefix RE of the trigger, and regexp2 is the suffix RE of the trigger. Roughly, the formula represents a conditional satisfaction such that whenever regexp1 holds, regexp2 should hold immediately afterward. Similar to the patterns mentioned above, the addition of triggers to Spectra is done by translating the trigger into a Büchi automaton and then using auxiliary variables, initial, safety, and justice constraints to embed it within the GR(1) specification. See [5].
Abstract Syntax of a Specification Some of the heuristics we present depend on the syntax of the specification. We repeat here the abstract syntax definition of a GR(1) specification, from [34].
Definition 1 (Abstract syntax of a specification)
A GR(1) specification is a tuple \(Spec = \langle V_e, V_s, D, M_e, M_s \rangle \), where \(V_e\) and \(V_s\) are sets of environment and system variables respectively, \(D : V_e \cup V_s \rightarrow Doms\) assigns a finite domain to each variable, and \(M_e\) and \(M_s\) are the environment and system modules. A module is a triplet \(M = \langle I, T, J \rangle \) that contains sets of initial assertions \(I = \{I_n\}_{n=1}^i\), safety assertions \(T = \{T_n\}_{n=1}^t\), and justice assertions \(J = \{J_n\}_{n=1}^j\) of the module, where \(i = |I|, t = |T|\) and \(j = |J|\). The set of elements of module \(M = \langle I, T, J \rangle \) is \(B_M = I \cup \{\textbf{G} T_i\}_{i=1}^t \cup \{\textbf{GF} J_i\}_{i=1}^j\).
2.3 Binary Decision Diagrams (BDDs) and Variable Ordering
All computations described above are performed symbolically using manipulations on Boolean functions. These are implemented using Binary Decision Diagrams (BDDs) [12], which are concise representations for Boolean functions that allow for fast manipulation.
The performance of BDD manipulation algorithms is highly sensitive to the ordering of variables within the BDD [13]. Finding an optimal variable ordering for BDDs is NP-hard [10]. As a result, heuristic approaches are employed to discover good orderings. These approaches are divided into two categories: dynamic variable reordering methods targeting the BDD level independently of the model, and static variable ordering using model-specific information.
3 Performance Heuristics
For each heuristics, we discuss motivation and background, present the heuristics itself, and consider its expected impact. Some of the heuristics apply to the realizability checking algorithm itself. Others are applied during the construction of the game model before the fixed-point computation starts. The heuristics are independent, meaning each can be applied regardless of the others. That said, some are related in the sense that in the presence of one, another is expected to become more effective. All our heuristics are conservatively sound, meaning they don’t alter the analysis result (except for one case, see Rem. 1). They only impact memory usage and computation time.
3.1 Memoryless Computation
The GR(1) synthesis algorithm, as presented in [9], retains fixed-point results throughout the computation process in order to facilitate the construction of a controller. This approach is implemented by default in notable GR(1) synthesizers like Spectra and Slugs [17]. However, for realizability checking alone, retaining these intermediate results is unnecessary.
Motivation Software development involves iterative steps of coding and debugging, just as specification development requires multiple cycles of realizability checks and refinements before finalizing the specification for controller construction. Ma’ayan and Maoz [27] recommend an iterative development scheme with frequent realizability checks, saving full synthesis for the final realizable specification, resulting in many checks without immediate controller construction.
Heuristics In [19], Firman et al. introduced several performance heuristics for GR(1) synthesis, including:
sca: combined conjunction and existential abstraction; eun: early detection of unrealizability; efp: early detection of fixed-point; and fpr: fixed-point recycling.Importantly, while the intermediate results are not necessary for realizability checking, some of the above heuristics rely on them. Specifically,
efp requires saving the intermediate Z fixed-point BDDs, and fpr requires saving the intermediate X fixed-point BDDs. We therefore consider two alternative heuristics: full memoryless: discards the X, Y, and Z fixed-point BDDs, and utilizes only sca and eun heuristics; and partial memoryless: discards only the Y fixed-point BDDs, and fully utilizes the four heuristics.Avoiding
efp might lead to worse performance on some unrealizable specs, and avoiding fpr is expected to increase the lengths of fixed-point iterations. Following preliminary experiments on a small arbitrary subset of specifications from our corpus, which confirmed the above weaknesses of the full memoryless alternative, we decided to employ the partial memoryless alternative in our work.Expected Impact We expect that our partial memoryless approach would reduce running times, not only thanks to faster sifting (or other dynamic reordering algorithms if used) but also thanks to a better variable ordering (intuitively, with fewer BDDs stored in memory, finding an effective ordering is easier).
3.2 Initial Static Variable Ordering
Motivation Considerable work has been done on static variable ordering for BDD-based models, e.g., [2‐4, 35]. To the best of our knowledge, it has not been attempted for GR(1) or LTL synthesis. We propose a static variable ordering heuristic that leverages GR(1) structure to put together semantically related variables. This creates a better starting point for the dynamic ordering method (specifically, sifting) used later in the GR(1) algorithm.
Heuristics Our approach follows ideas from [35], applied to our context of GR(1). We start by representing the GR(1) specification as a bipartite graph, where one set of nodes represents the specification’s variables (both unprimed and primed), and the other set of nodes represents the constraints, including initial, safety, and justice assumptions and guarantees, the Spectra constructs (triggers, counters, patterns), and the multiple constraints derived from them. An edge between a variable and a constraint means that the variable appears in the constraint’s support. The graph serves as an abstraction, only capturing relationships between specification elements and variables.
Next, we build the graph’s adjacency matrix and apply an off-the-shelf implementation of the classic Cuthill-McKee algorithm [15] (technically, its commonly used reversed variant), to minimize the matrix’s bandwidth, i.e., the distance of nonzeros to the diagonal of a matrix. Since Cuthill-Mckee only accepts symmetric matrices, we apply the symmetrization and de-symmetrization approach used in [35]. Reducing bandwidth roughly corresponds to our goal of making variables that are in the support of the same constraints closely ordered.
Expected Impact We hypothesize that complementing the dynamic ordering during the GR(1) algorithm with a good initial static ordering would positively impact performance. Minimizing the bandwidth is expected to put related variables (w.r.t. the constraints they appear in) close to each other.
That said, the initial ordering currently used by Spectra is not arbitrary - it follows the original variable declaration order from the specification and puts all unprimed and primed variables for each domain together. For human-written specifications, it is reasonable to assume that related variables are often close together in the specification file. Thus, currently implemented ordering may already be relatively effective, and it is not clear that our proposed heuristics would outperform it.
3.3 Justice Ordering
Motivation In GR(1) specifications, the environment and system justices represent fairness conditions. The order in which they are written in the specification doesn’t affect its semantics. However, we have performed preliminary experiments showing that their computation order in the fixed-point algorithm can significantly impact performance. The current implementation in Spectra follows the order in which the justices are originally written in the specification.
We propose a method to order the environment justices and system justices, each set separately, based on their relative importance in the specification structure. We hypothesize that trying to reach the most important justices first will improve the algorithm’s performance.
Heuristics To determine the relative importance of justices, we build a bipartite graph similar to the one presented earlier, i.e., where one set of nodes represents the specification’s variables, and the other set represents the constraints (initial, safety, and justice assumptions and guarantees). An edge between a variable and a constraint means that the variable appears in the constraint’s support.
To determine the importance of each justice, we use the eigenvalue centrality score (see, e.g., [11]), as implemented in the JGraphT [37] library. A popular adaption of eigenvalue centrality is PageRank [38]. We use the centrality score to reorder each set of justices, environment and system, in decreasing order.
Expected Impact Justice ordering is expected to positively affect the performance of the GR(1) realizability checking algorithm by potentially reaching fixed-points faster. Faster running time via a specific order is partly caused by a reduction in the total number of fixed-point iterations, as we have confirmed in our preliminary experiments.
Spectra already uses the order as it appears in the specification file. This order is already not random but typically based on the developer’s natural intention to put the most important constructs first or to put related constructs close to one another. We ran preliminary experiments that showed that this order is already much better than a random one. Therefore, in our evaluation in Sect. 4, we compare our heuristics to the original order, and not to a random one.
Finally, observe that our suggested order may outperform the specification file’s order not only by speeding up computation, but also by providing consistent performance, regardless of how the engineer chose to write the specification.
3.4 Simplified Automaton Embedding into GR(1)
Background and Motivation To allow for more concise specifications and easier expression of complex properties that capture LTL logic without a direct GR(1) equivalent (without additional variables), Spectra supports the use of specification patterns [16, 29] and triggers [5]. This support is systematically done in Spectra by embedding generated automata into the game model, using auxiliary variables. Although this is done inside the synthesizer and is completely transparent to the specification developer, it adds variables and justice constraints to the game model. It thus increases the specification’s complexity and state-space and in general results in a negative effect on performance.
Observation and Heuristics We observed that many of the specification patterns already defined in Spectra’s patterns library and potentially many of the triggers written by developers are currently encoded using a Büchi automaton with a justice acceptance condition. However, many of them are actually safety properties that can be encoded with fewer states and potentially fewer variables. Specifically, we found that 36 of the 51 patterns in the library can be expressed without a justice condition.
Definition 2 (dead-end state)
Given an automaton, a dead-end state is a state from which no accepting state of the automaton is reachable.
Spectra’s library of patterns was created by translating the patterns given as LTL formulas into minimal deterministic Büchi automata. Therefore, when an LTL formula at hand represents a safety property, its automaton includes a single dead-end state.
Given an automaton representing a pattern, we first remove its dead-end state (and its incoming and outgoing transitions), if any. We then check whether the remaining states are all accepting, and if so, remove the justice from the pattern’s representation for Spectra. Note that removing dead-end states does not change the language accepted by the automaton’s embedding into GR(1). Moreover, when all states are accepting, the added justice becomes trivially true and is therefore redundant.
For example, the pattern "p becomes true between q and r" appears in Spectra’s pattern library as shown in List. 1. In our new simplified automata library, the same pattern is defined as shown in List. 2. Specifically, note that the dead-end state
S2 and the justice from line 17 in List. 1 have been removed.Remark 1 (Effect on the Specification’s Semantics)
Interestingly, unlike all other heuristics we present in this work, this heuristics has a side effect on the semantics of the GR(1) specification. Specifically, due to the GR(1) semantics of strict realizability [9, 25], where the system may avoid satisfying its justice guarantees as long as the environment does not satisfy its justice assumptions, a specification that was regarded as realizable before the application of our heuristics, due to non-well-separation, will become unrealizable after the application of our heuristics (the justice guarantee violation is replaced with a safety guarantee violation). This side effect is actually desirable, as it prevents the system from taking advantage of non-well-separation and forcing the environment into assumption violation. Indeed, it may happen in realizability checking but cannot happen in kind-realizability checking (see [22, 28] and below).
Remark 2 (Simplification for Triggers)
The embedding of triggers into GR(1) in Spectra allows a similar simplification. In the general case, the translation adds a justice constraint to ensure that once reaching regexp2, eventually the automaton will start waiting again for regexp1. However, intuitively, if regexp2 includes no Kleene star or Kleene plus symbols (or an unbounded range), this eventuality is bounded (there is no cycle in the automaton corresponding to regexp2) and so the added justice is redundant. We thus apply a similar simplification heuristics of removing dead-ends and unnecessary justices to the automata generated by Spectra for triggers as well.
Expected Impact Based on the heuristics described above, out of the 51 Dwyer patterns defined in the Spectra library according to [29], 78.4% (40) had a dead-end state that can be removed, 70% (36) had a justice that can be removed, and 45% (23) resulted in the removal of one variable. The removal of a variable (one variable per pattern instance) makes the problem smaller. Moreover, the removal of justice(s) means fewer fixed-point loops to execute. Both the dead-end states and justice removals keep the semantics (see Rem. 1). Finally, applying the heuristics to the patterns library was done offline once, adding no overhead to realizability checking performance. Although applying them to triggers incurs a small overhead, it only affects a small automaton rather than the entire specification. Therefore, we expect these heuristics to improve performance.
3.5 Grouping of Auxiliary Variables
Motivation The original GR(1) setup does not explicitly handle auxiliary variables, but Spectra enhances it with high-level constructs such as patterns, triggers, and counters, which require auxiliary variables for embedding them within GR(1). We observe that these auxiliary variables are local, as they are used only by the constraints representing the pattern, trigger, or counter.
Heuristics Firman et al. [19] considered the grouping for each variable in \(V_e\) and \(V_s\), in pairs of primed and unprimed. However, their evaluation showed that this variable grouping approach might worsen performance for some specifications. We suggest a different approach, grouping only auxiliary variables that correspond to the same high-level construct instance.
Expected Impact As the auxiliary variables added for each language construct instance are semantically closely related and are not used directly by any constraint outside the construct instance, we expect that their grouping based on the construct instance they belong to would reduce BDD sizes and speed up BDD operations. Grouping is also expected to reduce dynamic reordering times, as reordering is done at the group level and not at the level of each variable alone.
3.6 Heuristics for Additional GR(1) Specification Analyses
All the above heuristics are relevant not only to the GR(1) realizability checking algorithm but also to other existing analyses for GR(1) specifications: non-well-separation, kind-realizability, and inherent vacuity.
Well-separation [25, 31] is a property of environment specifications that ensures the environment cannot be forced to violate its own assumptions, regardless of system behavior. Spectra includes an algorithm for detecting non-well-separated GR(1) specifications by reducing the problem to GR(1) realizability checking. We apply all the heuristics mentioned above to the non-well-separation detection in Spectra. Notably, detecting non-well-separation does not require guarantees, so we do not load them. We expect these heuristics to enhance the performance of non-well-separation detection.
Kind-realizability [22], following [28], uses a 4 fixed-points realizability checking algorithm that checks the existence of a strategy that ensures that the system does not exploit non-well-separated specifications, i.e., by forcing environment assumption violations. This 4 fixed-point algorithm, while capturing the concept of realizability in a more desired way, incurs significantly higher computational costs, as evident in experiments presented in [22, 28]. This limits its use in practice. We apply all the above heuristics to the kind-realizability checking implemented in Spectra.
Inherent vacuity [20] deals with redundant elements in a specification. Spectra includes an implementation of inherent vacuity detection for GR(1) [34], specifically identifying assumptions, guarantees, and variable values whose removal from the specification will not change its semantics. We apply all the above heuristics to the inherent vacuity detection implemented in Spectra. We further observe that in the case of redundant environment variable values, there is no need for the system guarantees and therefore do not load them at all. The application of all these heuristics is expected to improve the performance of inherent vacuity detection.
4 Evaluation
4.1 Specification Corpus, Implementation, and Validation
Specification Corpus We used two main sources for specifications. First, the SYNTECH set of benchmarks, which includes specifications written by CS students during semester-long project classes between 2015 and 2023, modeling and executing or simulating many robotic and other systems. They include not only final specifications but also many intermediate versions from the specification development process, and so, e.g., many unrealizable specifications. The SYNTECH benchmarks have been used in the evaluation of many previous works, e.g., [5, 14, 19, 22, 27, 36]. Second, Spectra versions of AMBA [7] and GenBuf [8], which are parametric specifications commonly used in the evaluation of GR(1) and related algorithms and are part of the SYNTCOMP benchmark [24].
The SYNTECH benchmark includes a total of 3390 specifications. We used 9 AMBA specifications (2 to 10 masters) and 14 GenBuf specifications (5 to 130 requests).
To evaluate the heuristics that relate to patterns and triggers, we focused on specific subsets of the SYNTECH specifications that already include at least one pattern or at least one trigger (but not necessarily ones that are amenable to our automata simplification heuristics). Out of the SYNTECH specs, 449 include at least one pattern and 173 of these include at least one pattern relevant to our heuristics. Similarly, 217 include at least one trigger and 176 of these include at least one trigger relevant to our heuristics (not all triggers in the benchmark can have their state/justice reduced; the heuristics applies only to triggers whose second SFA contains an unnecessary sink state, see Rem. 2). We name these SYNTECH-P and SYNTECH-T respectively.
To evaluate the heuristics that relate to well-separation, we used only the subset of realizable specifications from SYNTECH. We name it SYNTECH-R.
Implementation We have implemented our ideas on top of the Spectra GR(1) synthesizer [32] (with the heuristics of [19]), with a modified version of the CUDD BDD library, implemented in C [43]. The dynamic reordering method used is sifting. Other settings remain unchanged. We used the Cuthill-Mckee implementation available in the Boost C++ library [1].
Validation To validate the correctness of our ideas and implementation, we conducted extensive testing for each algorithm (GR(1), kind-realizability checking, well-separation, and inherent vacuity). Specifically, we compared the results from the public version of Spectra (i.e., without our heuristics), and our new implementation with heuristics, to check that they agree. We executed these tests on all specifications in our corpus.
The single case where the results may not agree, see Rem. 1, happened in realizability checking of exactly one specification that passed the lower bound filter (see below) from SYNTECH-T. As expected, it did not happen in the kind-realizability checks.
4.2 Experiment Setup and Reporting
We ran all experiments on an AWS t3.2xlarge instance (representing an ordinary laptop with up to 3.1GHz CPU and 32GB RAM) with Windows 10 64-bit OS, Java 11 64Bit, and CUDD 3 compiled for 64Bit, using one CPU core. Times we use are average values of 3 runs, measured in milliseconds. Although the algorithms we deal with are deterministic, we performed 3 runs as JVM garbage collection and the CUDD implementation of dynamic reordering add variance to running times. To simplify the presentation, we use a fixed table structure to report all results. We now explain the meaning of the columns in the table.
Columns Benchmark and #>60s: To focus on the cases where improving performance is more valuable, we filtered out from the experiment results for each benchmark all specifications where the original realizability checking by Spectra (with the heuristics of [19]) took less than 60 seconds. Column Benchmark presents the benchmark name and column #>60s shows how many of the specifications in this benchmark passed the lower bound filter. The remainder of the table refers to this number.
Columns R50%, R, and R<1: For each benchmark, we compute the geometric mean of the ratios between the time with the heuristics and the baseline time. That is, every number below 1.0 means that the heuristics had, on average, made the computation faster. The lower the number, the faster the heuristics relative to the baseline. We report two such average ratios, for the specifications whose baseline performance was slower than the median baseline performance and for the complete benchmark (after filtering and without timeouts, see below), in columns R50% and R resp. In addition, column R<1 reports the percentage of specifications (after filtering and without timeouts) for which the heuristics has improved running time, i.e., the percentage of specifications for which the ratio was below 1.0. The higher this percentage, the better the results compared to the baseline.
Columns B-TO and H-TO: To keep the cost of the experiments over hundreds of specifications reasonable, we set a timeout of 10 minutes for all experiments. When at least one of the algorithms, with or without the heuristics, reaches the timeout, we do not count it in the computed average ratios. Instead, in columns B-TO and H-TO we report the percentage of specifications that resulted in a timeout for the baseline and for the heuristics respectively.
Minor differences between the results in the two tables are expected as they report results from separate executions of the experiments and thus slightly different baselines.
4.3 Results
We aim to assess the impact of each heuristic on the performance of realizability checking and other analyses. Since the partial memoryless heuristic is expected to affect all algorithms, we first evaluate it against the original Spectra implementation. This partial memoryless version serves as a baseline for subsequent experiments, allowing us to evaluate the additional impact of the other heuristics. We conclude the report with a comparison of all our heuristics against the original Spectra implementation (without the partial memoryless heuristics). In all cases, we use Spectra with all the heuristics from [19].
Table 1.
Results for individual heuristics (measuring realizability checking times except the last two rows which refer to non-well-separation and inherent vacuity)
Dummy
Table 2.
Results for all heuristics together vs. Spectra
Analysis | Benchmark | #>60s | R50% | R | R<1 | B-TO | H-TO |
|---|---|---|---|---|---|---|---|
Real. check | SYNTECH | 268 | 0.45 | 0.49 | 80% | 16% | 12% |
AMBA+GenBuf | 12 | 0.35 | 0.60 | 83% | 42% | 0% | |
Well-sep. | SYNTECH-R | 197 | 0.62 | 0.75 | 83% | 0% | 0% |
AMBA+GenBuf | 12 | 0.14 | 0.27 | 100% | 8% | 0% | |
Kind. real. | SYNTECH | 268 | 0.46 | 0.57 | 79% | 53% | 42% |
AMBA+GenBuf | 12 | 0.20 | 0.48 | 67% | 33% | 0% |
The evaluation of individual heuristics appears in Table 1.
Partial Memoryless Computation We observe that for 268 specifications of the SYNTECH benchmark, the baseline realizability checking time was more than 60 seconds, and for these specifications, the heuristics performed approximately 5% faster on average, was faster in about 2/3 of the specifications, and resulted in slightly less cases of timeout compared to the Spectra baseline.
As expected, the use of partial memory did not change the number of fixed-point iterations. The reduction in total variable reordering time is mixed, as we observed (not shown in the table) a 15% reduction for SYNTECH and a 2% percent increase for AMBA+GenBuf. This partly explains the improvement we see in performance.
Static Variable Ordering We observe that on the SYNTECH benchmark the heuristics performed at least 40% faster on average, was faster in about 2/3 of the specifications, and resulted in roughly the same number of timeouts. On AMBA+GenBuf, it performed slightly slower on average, but still was faster in half of the specifications, and resulted in fewer timeouts.
Justice Ordering On the SYNTECH benchmark, the heuristics was up to 9% faster on average, was faster in almost 2/3 of the specifications, and resulted in the same number of timeouts. On AMBA+GenBuf, it performed much better on average, but was faster in only a quarter of the specifications, and resulted in more timeouts.
Note that in this heuristics and the previous one, we compare against the original ordering used by Spectra, which is not arbitrary but follows the order in which the variables and justices appear in the specification. Thus, the competition is expected to be tough.
Simplified Automaton Embedding and Grouping of Auxiliary Variables for Patterns and Triggers We observe that the heuristics performed at least 24% faster on average, with higher improvements for originally slow computations. We also observed that the heuristic was faster in at least 2/3 of the specifications in each corpus and resulted in fewer timeouts.
The reductions in running times are partly explained by reductions in the number of X fixed-points iterations (not shown in the table), 9%, 33%, and 79% reduction in the SYNTECH-P, SYNTECH-T, and AMBA corpora respectively.
Interestingly, for AMBA the improvement was exceptional. We investigated it and found that the Spectra specification of AMBA, which aims to formalize the requirements from [21], uses multiple patterns, for readability. For instance, guarantee G2: When a locked unspecified length burst starts, a new access does not start until the current master (i) releases the bus by lowering HBUSREQi, which in [21] is formalized using a long LTL formula with the until operator (and several additional operators), is formalized in the Spectra specification, for every i from 0 to N, as
P_becomes_true_between_Q_and_R(!hbusreq[i], locked_unspec_burst(i) & start, next(start)); These N patterns create redundant states and justice guarantees, which our heuristics detects and removes.
Heuristics for Additional Specification Analyses For non-well-separation detection (environment only), the heuristics performed at least 14% faster on average, and improved performance on 77% of the specifications.
For inherent vacuity detection (of redundant environment values), the heuristics performed at least 32% faster on average, and improved performance on at least 98% of the specifications.
All Heuristics Together Finally, Table 2 presents results for all heuristics together vs. Spectra, w.r.t. realizability checking, non-well-separation, and kind-realizability.
For the SYNTECH specifications realizability checking, we observe that our heuristics performed on average at least 2 times faster than Spectra, improved performance in 80% of the specifications, and resulted in less timeouts. For well-separation, we observe that our heuristics performed about 25% faster on average, and improved performance on 83% of the specifications. For kind-realizability, our heuristics performed at least 43% faster on average, improved performance in 79% of the specifications, and resulted in less timeouts.
We see similar and even mostly better results for the AMBA+GenBuf specifications.
The reductions in realizability checking running times are partly explained by the reductions in the number of X fixed-points iterations and the reductions in total variable reordering time - with R values of 0.85, 0.45 and R<1 values of 45%, 83% for these metrics respectively.
Why Do Some Specifications Resist Our Heuristics? We checked the characteristics of the 12% of specifications that reached the timeout despite the use of all heuristics (Table 2), compared to the other 88%, and found that the specifications in the first set have on average 42% more variables (101 compared to 70), 72% more pattern instances (1.9 / 1.1), 87% more trigger instances (1.5 / 0.8), and 43% more justice guarantees (6 / 4.2). A deeper analysis is required to better understand whether the challenge is primarily the size of these specifications and how additional heuristics may help.
5 Conclusion
We introduced heuristics to enhance the performance of GR(1) realizability checking and related algorithms. These heuristics are based on three observations: (1) many analyses in specification development do not require the intermediate results of the GR(1) algorithm’s fixed-point iterations, (2) the syntax of the specification, as written by developers, reveals insights into the structure of the GR(1) game model, offering opportunities for performance improvements, and (3) while high-level language constructs can simplify the writing and reading of complex specifications, they often incur hidden, redundant costs.
We implemented the heuristics and evaluated them over a large corpus of hundreds of GR(1) specifications written in the Spectra language. The results showed that compared to the previous implementation of the Spectra synthesizer, based on [19], each of the heuristics alone and all of them together result in faster realizability checking and other related analyses.
Artifact An artifact is available in https://doi.org/10.5281/zenodo.14616533. It includes the benchmarks used in our evaluation, raw data, and scripts to run and reproduce the experiments.
Acknowledgements
This research was supported by the Israel Science Foundation (grant No. 1954/23, SPECTACKLE) as well as by Len Blavatnik and the Blavatnik Family Foundation. The authors thank the anonymous reviewers and Rafi Shalom for helpful comments.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
