Realizability and reactive synthesis from temporal logics are fundamental problems in formal verification. The complexity of these problems for linear temporal logic with past (LTL+P ) led to the identification of fragments with lower complexities and simpler algorithms. Recently, the logic of extended bounded response LTL+P (\(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) for short) has been introduced. It allows one to express safety languages definable in LTL+P and it is provided with an efficient, fully symbolic algorithm for reactive synthesis. This paper features four related contributions. First, we introduce GR-EBR , an extension of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) with fairness conditions, assumptions, and guarantees that, on the one hand, allows one to express properties beyond the safety fragment and, on the other, it retains the efficiency of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) in practice. Second, we the expressiveness of GR-EBR starting from the expressiveness of its fragments. In particular, we prove that: (1) \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) is expressively complete with respect to the safety fragment of LTL+P , (2) the removal of past operators from \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) results into a loss of expressive power, and (3) GR-EBR is expressively equivalent to the logic GR(1) of Bloem et al. Third, we provide a fully symbolic algorithm for the realizability problem from GR-EBR specifications, that reduces it to a number of safety subproblems. Fourth, to ensure soundness and completeness of the algorithm, we propose and exploit a general framework for safety reductions in the context of realizability of (fragments of) LTL+P . The experimental evaluation shows promising results.
Hinweise
Communicated by Antonio Cerone and Frank de Boer.
This work is an extension of the conference papers [1, 2]
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
1 Introduction
One of the most important problems in formal methods and requirement analysis is establishing whether a specification over a set of controllable and uncontrollable actions is implementable (or realizable), that is, whether there exists a controller that chooses the value of the controllable actions and satisfies the specification, no matter what the values of uncontrollable actions are [5, 6]. This problem has been formalized in the literature under the name of realizability [3]. The very close problem of reactive synthesis aims at synthesizing such a controller, whenever the specification is realizable. Usually, these problems are modelled as two-player games between Environment, who tries to violate the specification, and Controller, who tries to fulfill it. Realizability is known to have a very high worst-case complexity. In particular, it has a non-elementary lower bound for S1S specifications [4], and it is 2EXPTIME-complete for Linear Temporal Logic (LTL ) specifications [5, 6].
In order to apply realizability and reactive synthesis in real-world scenarios, research has focused on the identification of fragments of S1S and LTL , with a limited expressive power, for which realizability can be solved efficiently.
Anzeige
A well-known example is Generalized Reactivity(1) (GR(1) , for short) [7]. In this fragment, a specification is syntactically partitioned into assumptions about the environment and guarantees for the controller. Both of them are either Boolean formulas (say, \(\alpha \)) or safety formulas (\(\textsf {G} \alpha \)) or conjunctions of recurrence formulas (\({\bigwedge _{i=1}^{n} \textsf {GF} \alpha _i}\)). The dichotomy between assumptions and guarantees reflects the way a system engineer usually formalizes system requirements, which is summarized by the following sentence: “the controller has to behave in conformance to the guarantees, under the given assumptions on the environment".
On a different direction, other approaches focused on safety fragments of Linear Temporal Logic with Past (LTL+P ) [8, 9]. In particular, Extended Bounded ResponseLTL+P (\(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , for short) is a safety fragment of LTL+P with the following features [9]: (i) its realizability problem is EXPTIME -complete; (ii) there exists a fully symbolic compilation of its formulas into deterministic automata. This last feature, in particular, contributes to a great improvement in solving time for the synthesis problem.
A second research direction on reactive synthesis focuses on finding good algorithms for the average case. Among these, an important class of algorithms makes use of the so-called safety reductions, that reduce the realizability problem for the original formula to a sequence of subproblems for safety formulas by bounding some behaviors of the former, e.g., the visits to the rejecting states of the corresponding automaton, by some integer k. The rationale behind these techniques is that a safety problem is usually much simpler to solve, since it amounts to a strong reachability problem [10]. This is in turn inspired by safety reductions for the model checking problem, where the validity of an LTL formula over a Kripke structure is reduced to checking the reachability of a given error state [11, 12]. Usually, safety reductions (for both realizability and model checking) are: (i) sound, meaning that a positive answer to any of the subproblems implies a positive result of the original formula, and (ii) complete, ensuring that there exists an upper bound \(\mu \) such that, if the k-th subproblem has a negative answer for all \(k \le \mu \), then also the result for the original formula is negative. Meaningful examples of safety reductions for realizability are the contributions on bounded synthesis [13], which are based on the pioneering work on Safraless algorithms [14], and all the different encodings proposed for solving it [15].
1.1 Contributions
The main contributions of the paper are the following ones.
Anzeige
First, we introduce the logic of Generalized Reactivity(1)\(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) (GR-EBR , for short), an extention of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) that admits:
1.
fairness conditions, in particular conjunctions of recurrence formulas, that is, \({\bigwedge _{i} \textsf {GF} \alpha _i}\), forcing each formula \(\alpha _i\) to be true infinitely often;
2.
assumptions/guarantees in the form of an \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) formula augmented with fairness conditions.
In addition to make it possible to express any \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) formula, GR-EBR also allows one to define properties that are not captured by the safety fragment, like, for instance, \(\textsf {G} p\rightarrow \textsf {G} q\).
Second, we investigate the expressiveness of GR-EBR . We begin with the analysis of the expressive power of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , which, by definition, is a fragment of GR-EBR , and we prove that it can express all and only the safety properties that are definable in LTL+P . A crucial role in the proof of such an expressive equivalence is played by past temporal modalities of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) . Then, we prove that they are really necessary by showing that the logic \(\textsf {LTL} _\textsf {EBR} \) , that is, the fragment of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) where past modalities have been removed, is strictly less expressive than \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) . Finally, by exploiting the previous results, we demonstrate that GR-EBR is expressively equivalent to GR(1) [7].
Third, we study the reactive synthesis problem for GR-EBR . In particular, we give an algorithm that, at each iteration, builds a safety subproblem and checks its realizability. If it returns a positive result, then the initial formula is realizable as well, and a controller implementing the specification can be effectively built; otherwise, it continues with the next iteration. If the upper bound given by the reduction has been reached, the algorithm outputs the unrealizability of the initial formula. As a matter of fact, the upper bound is doubly exponential in the size of the formula and thus prohibitively large. For this reason, in practice, it is useful to use the algorithm in parallel with another one checking for the unrealizability of the formula. The first that terminates stops the other and, thus, the entire procedure. A crucial property of the algorithm is that the realizability check of each safety subproblem is performed in a fully symbolic way, thus retaining the distinctive feature of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) .
Fourth, we prove the correctness of the proposed algorithm for realizability. To this end, we devise a novel framework for deriving complete safety reductions in the context of realizability of (fragments of) LTL+P . A notable feature of the framework is that it provides a link to safety reductions for model checking, by showing that if a reduction is complete for model checking, then it is complete for realizability as well. On the one hand, this allows one to reason on Kripke structures instead of strategies, which is simpler; on the other hand, it enables the use of some reductions already exploited in model checking for realizability, provided that they conform to the framework. We use the framework to derive a complete safety reduction for the realizability problem of GR-EBR . Moreover, we show how to apply it to prove the completeness of Bounded Synthesis [13] using the K-Liveness reduction to safety [11].
Last but not least, we provide an implementation of the algorithm as a prototype tool called grace (GR-ebr reAlizability ChEcker). The experimental evaluation shows good performance against tools for full LTL+P synthesis.
adding a characterization of the exact expressive power of GR-EBR ;
2.
providing the complete proofs of all lemmata and theorems;
3.
describing in detail the formalization of Bounded Synthesis in terms of the proposed general framework;
4.
improving the analysis of related work.
1.2 Relevance for SoSyM
The relevance of the present work for a journal like the International Journal on Software and Systems Modeling (SoSyM) is manyfold. It proposes a novel formalism to express meaningful temporal properties, and pairs it with some effective techniques to check their realizability. The latter feature is fundamental in the context of correct-by-construction design; moreover, it turns out to be quite useful in the process of specification debugging: while satisfiability checks fail to establish whether a specification is implementable, realizability can be successfully employed to solve this task.
1.3 Organization
The rest of the paper is organized as follows. In Sect. 2, we introduce basic notation and definitions. In Sect. 3, we define the logic GR-EBR and we give an example of GR-EBR specification. In Sect. 4, we determine the expressive power of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , \(\textsf {LTL} _\textsf {EBR} \) , and GR-EBR . The symbolic algorithm that solves GR-EBR realizability is given in Sect. 5. In Sect. 6, we describe the framework for deriving complete reductions and we apply it to the case of GR-EBR , proving completeness of the algorithm described in the previous section. In Sect. 7, we analyse related work. The outcomes of the experimental evaluation are reported in Sect. 8. Finally, in Sect. 9, we point out some interesting future research directions.
2 Preliminaries
2.1 Temporal logics
Linear Temporal Logic with Past (LTL+P ) is a modal logic interpreted over infinite state sequences. Let \(\Sigma \) be a set of proposition letters. LTL+P formulas are inductively defined as follows:
where \(p \in \Sigma \). Temporal operators can be partitioned into future operators (next (\(\textsf {X} \)) and until (\(\textsf {U} \))) and past operators (yesterday (\(\textsf {Y} \)) and since (\(\textsf {S} \))). We define the following common abbreviations, where \(\top \) stands for any tautology, e.g., \(p\vee \lnot p\): (i) release: \(\phi _1\, \textsf {R} \, \phi _2 \equiv {\lnot (\lnot \phi _1\, \textsf {U} \, \lnot \phi _2)}\); (ii) eventually: \(\textsf {F} \phi _1 \equiv {\top \, \textsf {U} \, \phi _1}\); (iii) globally: \(\textsf {G} \phi _1 \equiv {\lnot \, \textsf {F} \, \lnot \phi _1}\); (iv) once: \(\textsf {O} \phi _1 \equiv {\top \, \textsf {S} \, \phi _1}\); (v) historically: \(\textsf {H} \phi _1 \equiv {\lnot \, \textsf {O} \, \lnot \phi _1}\); (vi) weak yesterday: \(\textsf {Z} \phi _1 \equiv {\lnot \, \textsf {Y} \, \lnot \phi _1}\). We say that an LTL+P formula is pure past if (and only if) all its temporal operators are past operators. We call pure pastLTL+P , written as \(\textsf {LTL{+}P} _\textsf {P} \) , the fragment of LTL+P containing only pure past formulas. Moreover, we denote by \(\textsf {LTL{+}P} _\textsf {BF} \) the Bounded Future fragment of LTL+P , that is, the fragment of LTL+P where the only admitted future temporal modality is \(\textsf {X} \).
Formulas of LTL+P are interpreted over state sequences. A state sequence\(\sigma =\langle \sigma _0,\sigma _1,\dots \rangle \) is an infinite, linearly ordered sequence of states, where each state \(\sigma _i\) is a set of proposition letters, that is, \(\sigma _i \in 2^\Sigma \), for \(i \in \mathbb {N}\). We will interchangeably use the term \(\omega \)-word over the alphabet \(2^\Sigma \) to refer to a state sequence. A set of \(\omega \)-words is called \(\omega \)-language. Given two indices \(i,j \in \mathbb {N}\), with \(i \le j\), we denote by \(\sigma _{[i,j]}\) the interval of \(\sigma \) from index i to index j, that is, \(\langle \sigma _{i},\dots ,\sigma _{j}\rangle \) if \(i \ge 0\), or \(\langle \sigma _{0},\dots ,\sigma _{j}\rangle \) otherwise. Finally, we denote by \(\sigma _{[i,\infty ]}\) the (infinite) suffix of \(\sigma \) starting from i.
Given a state sequence \(\sigma \), a position \(i\ge 0\), and an LTL+P formula \(\phi \), we inductively define the satisfaction of \(\phi \) by \(\sigma \) at position i, written as \(\sigma ,i\models \phi \), as follows:
\(\sigma ,i \models {\phi _1\, \textsf {U} \, \phi _2}\) iff there exists \(j\ge i\) such that \(\sigma ,j\models \phi _2\), and \(\sigma ,k\models \phi _1\) for all k, with \(i \le k < j\);
7.
\(\sigma ,i \models {\phi _1\, \textsf {S} \, \phi _2}\) iff there exists \(j\le i\) such that \(\sigma ,j\models \phi _2\), and \(\sigma ,k\models \phi _1\) for all k, with \(j < k \le i\);
We say that \(\sigma \)satisfies\(\phi \), written as \(\sigma \models \phi \), if it satisfies the formula at the first state, that is, if \(\sigma ,0\models \phi \): in this case, we say that \(\sigma \) is a model of \(\phi \). We say that two formulas \(\phi \) and \(\psi \) are equivalent (\(\phi \equiv \psi \)) if and only if they are satisfied by the same set of state sequences.
2.2 Notation
Let \(\phi \) be a LTL+P formula. We define the language of \(\phi \), denoted by \(\mathcal {L}(\phi )\), as \(\mathcal {L}(\phi ) = \{ \sigma \in (2^\Sigma )^\omega \vert \,\sigma \models \phi \}\). If \(\phi \) contains only past operators, we change the definition of the language of \(\phi \) as follows: for all \(\phi \in {\textsf {LTL{+}P} _\textsf {P} }\,\), the language of \(\phi \) over finite words is \(\mathcal {L}^{<\omega }(\phi ) {:=}\{\sigma \in (2^\Sigma )^* \vert \,{\sigma = \langle \sigma _0,\dots ,\sigma _n\rangle \text { and } \sigma ,n \models \phi }\}\).
From now on, given a linear temporal logic \(\mathbb {L}\), with some abuse of notation, we will denote by \(\mathbb {L}\) also the set of formulas that syntactically belong to \(\mathbb {L}\). Conversely, we denote by \(\llbracket \mathbb {L}\rrbracket \) the set of all and only those languages \(\mathcal {L}\) of infinite words for which there is a formula \(\phi \in \mathbb {L}\) (i.e., \(\phi \) syntactically belongs to \(\mathbb {L}\)) such that \(\mathcal {L}= \mathcal {L}(\phi )\). For the logic \(\textsf {LTL{+}P} _\textsf {P} \) , we denote by \(\llbracket {\textsf {LTL{+}P} _\textsf {P} }\,\rrbracket ^{<\omega }\) the set of languages \(\mathcal {L}\) over finite words such that \(\mathcal {L}= \mathcal {L}^{<\omega }(\phi )\) for some \(\phi \in {\textsf {LTL{+}P} _\textsf {P} }\,\).
Notice that, since past modalities do not add expressive power to LTL [16‐18], \(\llbracket \textsf {LTL} \,\rrbracket \) is the same as \(\llbracket \textsf {LTL{+}P} \,\rrbracket \).
2.3 \(\omega \)-regular expressions and (co-)safety classes
Let \(\textsf {REG} \,\) be the set of regular languages of finite words [19]. An \(\omega \)-regular language is a set of \(\omega \)-words recognized by an \(\omega \)-regular expression, that is, an expression of the form \(\bigcup _{i=1}^{n} U_i \cdot (V_i)^\omega \), where \(n \in \mathbb {N}\) and \(U_i,V_i \in \textsf {REG} \,\) for \(i=1,\dots ,n\). We denote the set of \(\omega \)-regular languages by \(\omega \)-REG . One of the seminal results in automata theory is the correspondence between \(\omega \)-regular languages and Büchi automata [20, 21]. An important class of \(\omega \)-regular languages is the class of those languages preventing something “bad”, e.g., a deadlock or a simultaneous access to a critical section by different processes, from happening. Languages in this class are called safety languages or, equivalently, safety properties.
Let \(\mathcal {L}\subseteq \Sigma ^\omega \) be an \(\omega \)-regular language. We say that \(\mathcal {L}\) is a safety language if and only if for all the words \(\sigma \in \Sigma ^\omega \) it holds that, if \(\sigma \not \in \mathcal {L}\), then \(\exists i \in \mathbb {N}\cdot \forall \sigma ^\prime \in \Sigma ^\omega \cdot \sigma _{[0,i]}\cdot \sigma ^\prime \not \in \mathcal {L}\). The class of safety \(\omega \)-regular languages is denoted by SAFETY .
Let \(\mathbb {L}\) be a temporal logic. We say that \(\mathbb {L}\) is a safety fragment of LTL+P if and only if \(\mathbb {L}\subseteq \textsf {LTL{+}P} \,\) and \(\mathcal {L}(\phi )\) is a safety language (Def. 1), for all formulas \(\phi \in \mathbb {L}\). A formula \(\phi \) is called a safety formula if \(\mathcal {L}(\phi )\) is a safety language.
Besides SAFETY , we introduce the class of (\(\omega \)-regular) co-safety languages, called coSAFETY , which is defined as the dual of SAFETY , i.e., \(\mathcal {L}\in \textsf {coSAFETY} \,\) if and only if \(\overline{\mathcal {L}} \in \textsf {SAFETY} \,\), where \(\overline{\mathcal {L}}\) is the complement language of \(\mathcal {L}\).
We give an alternative, equivalent definition of the SAFETY class of Def. 1, that will be useful in the following:
We define the class \(\textsf {SAFETY} ^{\textsf {SF} }\) (\(\textsf {coSAFETY} ^{\textsf {SF} }\) ) as the set obtained from SAFETY (resp. coSAFETY ) by restricting K to be a star-free expression, that is, a regular expression devoid of the Kleene star [23]. In particular, \(\textsf {coSAFETY} ^{\textsf {SF} }\,{:=}\{\mathcal {L}\subseteq \Sigma ^\omega \vert \,\mathcal {L}= K \cdot \Sigma ^\omega \wedge K \in \textsf {SF} \,\}\), where \(\textsf {SF} \,\subseteq \textsf {REG} \,\) is the set of star-free regular expressions. With \(\omega {\text{- }}\textsf {SF} \) we denote the set of star-free \(\omega \)-regular expressions. We recall that star-free expressions (SF ) and pure-past LTL (\(\textsf {LTL{+}P} _\textsf {P} \) ) have the same expressive power. The same holds for the \(\omega {\text{- }}\textsf {SF} \) class and LTL .
We will use the following normal-form theorem, stated in [25], that proves that any LTL -definable safety (resp., co-safety) language can be expressed by a formula of the form \(\textsf {G} \alpha \) (resp., \(\textsf {F} \alpha \)), where \(\alpha \in {\textsf {LTL{+}P} _\textsf {P} }\,\), and vice versa. An independent proof of such a theorem can be derived from the results by Thomas in [24]. Hereafter, we will denote by \(\llbracket \textsf {G} \alpha \rrbracket \) (resp., \(\llbracket \textsf {F} \alpha \rrbracket \)) the set of \(\omega \)-languages recognized by a formula of the form \(\textsf {G} \alpha \) (resp., \(\textsf {F} \alpha \)) with \(\alpha \in {\textsf {LTL{+}P} _\textsf {P} }\,\).
The logic Safety-LTL [8, 25, 26] is defined as the set of LTL formulas such that, when in negated normal form, do not contain existential temporal operators (i.e., \(\textsf {U} \) and \(\textsf {F} \)). Safety-LTL is a safety fragment of LTL [26]. In [25], it is proved that Safety-LTL is expressively complete with respect to the safety fragment of LTL+P .
A summary of the expressiveness of the considered logics is given in Fig. 1. Note that the intersection of SAFETY , coSAFETY and \(\llbracket \textsf {LTL{+}P} \,\rrbracket \) is not empty, since there are languages that are definable in LTL+P and are both safety and co-safety, like, for example, the language of the formula \(\textsf {XXX} (\textsf {Y} q \wedge \textsf {Y} p)\).
Fig. 1
A comparison of the expressiveness of the considered logics
×
2.4 The reactivity classes
In the following, we briefly recall the Temporal Hierachy defined by Manna and Pnueli in [27]. The top class in the hierarchy is the class Reactivity(N), which consists of all and only the formulas of the form:
where \(\alpha _i,\beta _i \in {\textsf {LTL{+}P} _\textsf {P} }\,\), for \(i=1,\dots ,N\), for some \(N \in \mathbb {N}\).
We denote the classes Reactivity(1), ..., Reactivity(N) by R(1) , ..., R(N) , respectively. It is known that LTL is exactly as expressive as the union of Reactivity(N), for all \(N\in \mathbb {N}\).
In [7], Bloem et al. introduced a logic obtained from Reactivity(1) by increasing the number of subformulas of the form \(\textsf {GF} \) that a formula can contain, maintaining the constraint of having only one implication. The resulting class, called Generalized Reactivity(1), is defined as follows.
Definition 2
(GR(1) [7]) Generalized Reactivity(1) (\(\textsf {GR(1)} \,\) for short) is the set of all and only the formulas of the form \((\alpha _I \wedge \textsf {G} (\alpha _T) \wedge \bigwedge _{i=1}^{m} \textsf {GF} \alpha _i) \rightarrow (\beta _I \wedge \textsf {G} ( \beta _T) \wedge \bigwedge _{j=1}^{n} \textsf {GF} \beta _j)\), where (i) \(\alpha _I, \beta _I\) are Boolean formulas, (ii) \(\alpha _T, \beta _T\) are \(\textsf {LTL{+}P} _\textsf {BF} \) formulas, where modality \(\textsf {X} \) can only occur in a non-nested form, and (iii) \(\alpha _i,\beta _j\) are \({\textsf {LTL{+}P} _\textsf {P} }\,\) formulas, for all \(i\in \{1,\dots ,m\}\) and \(j\in \{1,\dots ,n\}\), for some \(m,n \in \mathbb {N}\).
2.5 Extended bounded response LTL+P
Extended Bounded ResponseLTLwith Past (\(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , for short) is a fragment of LTL+P , which has been recently introduced in the context of reactive synthesis [9]. Below, we recall its syntax.
Definition 3
(The logic\(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) [9]) Let \(a,b \in \mathbb {N}\). An \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) formula \(\chi \) is inductively defined as follows:
where the bounded until operator \({\psi _1\, \textsf {U} ^{[a,b]}\psi _2}\) is a shorthand for the LTL formula \(\bigvee _{i=a}^{b} ( \textsf {X} ^i(\psi _2) \wedge \bigwedge _{j=0}^{i-1} \textsf {X} ^j (\psi _1))\), with \(\textsf {X} ^n \psi = \psi \) if \(n=0\), and \(\textsf {X} ^n \psi = \textsf {X} \textsf {X} ^{n-1}\psi \) otherwise (for all \(n\in \mathbb {N}\) and all \(\psi \in \textsf {LTL{+}P} \,\)). A bounded eventually operator \(\textsf {F} ^{[a,b]}\phi _1\) can be defined as \(\top \textsf {U} ^{[a,b]}\phi _1\). Similarly, we define the bounded globally operator \(\textsf {G} ^{[a,b]}\phi _1\) as \(\lnot \textsf {F} ^{[a,b]}\lnot \phi _1\). Since \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) features only past temporal modalities and the tomorrow, the release and the bounded until future temporal modalities, it is a safety fragment of LTL (see Theorem 3.1 in [26]).
The syntax of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) is articulated over layers, that impose some syntactic restrictions on the formulas that can be generated by the grammar. As an example, \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) forces the first argument of any release operator to contain no further \(\textsf {R} \) or \(\textsf {G} \) modalities.1
Any formula of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) can be rewritten into an equivalent formula in the following normal form.
Definition 4
(Normal Form of\(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) [9]) The normal form of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) is the set of all and only the formulas of the following type:
We define \(\textsf {LTL} _\textsf {EBR} \) as the fragment of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) devoid of the pure past layer.
Definition 5
(The logic\(\textsf {LTL} _\textsf {EBR} \) ) The logic \(\textsf {LTL} _\textsf {EBR} \) is obtained from \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) by removing past temporal operators.
2.6 Automata
The relationships between temporal logic and automata on infinite words have been extensively and successfully investigated in the literature (see, for instance, [28]). In the following, we will focus our attention on symbolic representations, which can be exponentially more succinct than the explicit-state one. Thus, we restrict our attention to symbolic automata, which are defined as follows.
Definition 6
(Symbolic automaton on infinite words) A symbolic automaton on infinite words over the alphabet \(\Sigma \) is a tuple \(\mathcal {A}= (V, I, T, \alpha )\), where (i) \(V=X\cup \Sigma \), with X a set of state variables and \(\Sigma \) a set of input variables, (ii) I(X) and \(T(X,\Sigma , X^\prime )\), with \(X'=\{x' \mid x\in X\}\), are Boolean formulas which define the set of initial states and the transition relation, respectively, and (iii) \(\alpha (X)\) is an LTL+P formula over the variables in X which defines the accepting condition.
The variables \(x'\) in \(X'\) are called the primed version of the variables x in X, and are supposed to represent the value of x in the next state.
We will make use of deterministic symbolic automata, which are defined as follows.
Definition 7
(Deterministic symbolic automaton on infinite words) A symbolic automaton \(\mathcal {A}= (V, I, T, \alpha )\), with \(V = X \cup \Sigma \), is deterministic iff (i) the formula I has exactly one satisfying assignment, and (ii) the transition relation is of the form:
where \(\beta _x(V)\) is a Boolean formula over V, for each \(x \in X\).
Symbolic automata over infinite words recognize a set of infinite words, called the language of the automaton, which is defined as follows.
Definition 8
(Language of a symbolic automaton) Let \(\mathcal {A}= (V, I, T, \alpha )\) be a symbolic automaton. A run \(\tau = \langle \tau _0,\tau _1,\dots \rangle \) is an infinite sequence of states (evaluations of the variables in X) such that any two consecutive states (evaluations) satisfy the formula T, for some assignment to the variables in \(\Sigma \). A run \(\tau \) is induced by the word \(\sigma \) iff \(\tau _0 \models I\) and \((\tau _i, \sigma _i, \tau _{i+1}) \models T\), for all \(i \ge 0\). A run \(\tau \) is accepting iff \(\tau \models \alpha \). A word \(\sigma \) is accepted by \(\mathcal {A}\) iff there exists an accepting run induced by \(\sigma \) in \(\mathcal {A}\). The language of \(\mathcal {A}\), denoted by \(\mathcal {L}(\mathcal {A})\), is the set of all and only the infinite words accepted by \(\mathcal {A}\).
We define the following classes of symbolic automata over infinite words, which differ from each other in the acceptance condition.
Definition 9
(Safety Automata,R(1)Automata, andGR(1)Automata) Let \(\mathcal {A}= (V, I, T, \alpha )\) be a symbolic automaton over infinite words. We say that \(\mathcal {A}\) is
a safety automaton iff \(\alpha {:=}\textsf {G} \beta \);
where \(\beta ,\beta ^\prime ,\beta _i,\beta _j^\prime \in {\textsf {LTL{+}P} _\textsf {P} }\,\) and \(m,n \in \mathbb {N}\).
2.7 Model checking, realizability, and synthesis
We conclude the section by formally stating the problems of model checking, realizability, and synthesis. As a preliminary step, we recall the notion of (finite) Kripke structure.
Definition 10
(Kripke structure) A Kripke structure is a tuple \(M=(\Sigma , Q, I, T, L)\), where
1.
\(\Sigma \) is the input alphabet;
2.
Q is the (finite) set of states;
3.
\(I \subseteq Q\) is the set of initial states;
4.
\(T \subseteq Q \times Q\) is a complete transition relation;
5.
\(L: Q \rightarrow 2^{\Sigma }\) is the labeling function that assigns to each state the set of proposition letters in \(\Sigma \) that are true in it.
We denote the number of states in M, i.e., |Q|, by |M|. A infinite trace of M is a sequence of states such that any consecutive pair of states \((q_i, q_{i+1})\) in it belongs to T. Given a trace \(\pi {:=}\langle q_0,q_1,\dots \rangle \) in M, we denote by \(L(\pi )\) the sequence \(\langle L(q_0), L(q_1), \dots \rangle \). A path \(\pi \) is called initialized if and only if \(q_0 \in I\).
The model checking problem takes as input a Kripke structure and a temporal formula, and verifies whether or not all the initialized traces of the former satisfy the latter.
Definition 11
(Model checking forLTL+P ) Let M be a Kripke structure and \(\phi \) be an LTL+P temporal formula. The model checking problem is the problem of verifying whether or not for all initialized traces \(\pi \) of M, it holds that \(L(\pi ) \models \phi \), written \(M \models \textsf {A} \phi \), where \(\textsf {A} \) is the “for all paths” modality of CTL.
Realizability and reactive synthesis are, in some sense, more ambitious than model checking, as they aim at establishing whether a given temporal formula \(\phi \) over two sets \(\mathcal {U}\) and \(\mathcal {C}\) of uncontrollable and controllable variables, respectively, is implementable and, if this is the case, to synthesize a possible implementation. Realizability is usually modeled as a two-player game between Environment, who tries to violate the specification, and Controller, who tries to fulfill it. In this setting, an implementation of the specification is represented by a strategy.
Definition 12
(Strategies and languages of strategies) Let \(\mathcal {U}\) and \(\mathcal {C}\) be two disjoint sets of input (or uncontrollable) and output (or controllable) variables, respectively. A strategyg is a function \(g: (2^{\mathcal {U}})^{+} \rightarrow 2^{\mathcal {C}}\) (where \((2^{\mathcal {U}})^{+}\) is the set of finite, non-empty sequences of elements in \(2^{\mathcal {U}}\)). The language of the strategy g, denoted by \(\mathcal {L}(g)\), is the set of all and only the sequences \(\langle (\textsf {U} _0 \cup \textsf {C} _0), (\textsf {U} _1 \cup \textsf {C} _1),\dots \rangle \) such that \(\textsf {U} _i \in 2^\mathcal {U}\) and \(\textsf {C} _i = g(\langle \textsf {U} _0, \dots , \textsf {U} _{i}\rangle )\), for all \(i \ge 0\).
Definition 13
(Realizability and synthesis forLTL+P ) Let \(\phi \) be an LTL+P temporal formula over \(\Sigma = \mathcal {U}\cup \mathcal {C}\), where \(\mathcal {U}\) is the set of input variables, \(\mathcal {C}\) the set of output variables, and \(\mathcal {U}\cap \mathcal {C}= \emptyset \). We say that \(\phi \) is realizable if and only if there exists a strategy \(g: (2^{\mathcal {U}})^{+} \rightarrow 2^{\mathcal {C}}\) such that \(\mathcal {L}(g) \subseteq \mathcal {L}(\phi )\). If \(\phi \) is realizable, the synthesis problem is the problem of computing such a strategy.
The strategies we are mainly interested in are those that can be represented finitely. In the literature, there are two main (and equivalent) representations of finite strategies, namely, Mealy machines and Moore machines. In this paper, we focus on the first ones.
Definition 14
(Mealy machine) A Mealy machine is a tuple \(M=(\Sigma _{\mathcal {U}}, \Sigma _{\mathcal {C}}, Q, q_0, \delta )\), where
1.
\(\Sigma _{\mathcal {U}}\) and \(\Sigma _{\mathcal {C}}\) are the input and output alphabets, respectively;
2.
Q is the (finite) set of states and \(q_0\) is the initial state;
3.
\(\delta : Q \times \Sigma _{\mathcal {U}} \rightarrow \Sigma _{\mathcal {C}} \times Q\) is the total transition function.
We say that an infinite word \(\sigma = \langle \sigma _0, \sigma _1, \dots \rangle \in (\Sigma _\mathcal {U}\cup \Sigma _\mathcal {C})^\omega \) is accepted by M iff there exists a trace\(\langle (q_0,\sigma _0), (q_1,\sigma _1), \dots \rangle \in (Q \times (\Sigma _\mathcal {U}\cup \Sigma _\mathcal {C}))^\omega \) such that \(\delta (q_i,\sigma _i \cap {\Sigma _\mathcal {U}}) = (\sigma _i \cap {\Sigma _\mathcal {C}}, q_{i+1})\), for all \(i \ge 0\). The language of M, denoted by \(\mathcal {L}(M)\), is the set of all the infinite words accepted by M.
A fundamental feature of the realizability problem for LTL+P is the following small model property [5, 14, 29], which ensures that each realizable LTL+P formula has at least one finitely representable strategy.
Proposition 2
(Small model property of LTL+P [5]) Let \(\phi \) be an LTL+P formula and \(n = |\phi |\). If \(\phi \) is realizable by a strategy g, then there exists a Mealy machine \(M_g\) such that (i) \(M_g\) has at most \(2^{2^{c \cdot n}}\) states, for some constant \(c \in \mathbb {N}\), and (ii) \(\mathcal {L}(M_g) \subseteq \mathcal {L}(\phi )\).
Notice that the constant c in Prop. 2 depends on the algorithms used for building the nondeterministic Büchi automaton for the language \(\mathcal {L}(\phi )\) and on the algorithms for its determinization (e.g., Safra’s algorithm [30] or alternating cycle decomposition [31]) to obtain an equivalent deterministic Rabin automaton (see [5]). It immediately follows that c can be effectively computed, obtaining a concrete upper bound for the size of the Mealy machine in Prop. 2.
In general, the realizability problem for an LTL+P formula can be reduced to a Büchi game [32], that requires the player Controller to visit infinitely often a state (or a set of states) in the arena. In the case of safety specifications, the full power (and complexity) of Büchi games is not necessary. Safety games [33, 34] are indeed a restriction of Büchi games, where the goal of Controller is to visit only states in a given set, called safe states.
Definition 15
(Safety game) Let \(\mathcal {A}= (V,I,T,\alpha )\) be a symbolic deterministic safety automaton (see Def. 9) such that \(V = X \cup \Sigma \), and \(\Sigma = \mathcal {C}\cup \mathcal {U}\), with \(\mathcal {C}\cap \mathcal {U}=\emptyset \), and \(\alpha {:=}\textsf {G} (\beta )\), with \(\beta \in {\textsf {LTL{+}P} _\textsf {P} }\,\). A safety game is a triple \(G=\langle \mathcal {A}, \mathcal {C}, \mathcal {U}\rangle \). We say that Controller wins G iff there exists a strategy \(g: (2^\mathcal {U})^{+} \rightarrow 2^\mathcal {C}\) such, for all sequences \(\textsf {U} =\langle \textsf {U} _0, \textsf {U} _1, \dots \rangle \in (2^\textsf {U} )^\omega \), the run \(\tau \) induced by \(\textsf {U} =\langle \textsf {U} _0 \cup g(\textsf {U} _0), \textsf {U} _1 \cup g(\textsf {U} _0,\textsf {U} _1), \dots \rangle \) in \(\mathcal {A}\) is accepting, that is, it only visits states \(\tau \) (i.e., evaluations of the variables in X) such that \(\tau \models \beta \).
In the following, we will reduce the realizability problem for GR-EBR to a sequence of safety games.
3 The logic of GR-EBR
In this section, we introduce the logic Generalized Reactivity(1)\(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) (GR-EBR , for short), an extension of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) with fairness conditions of the form \(\textsf {GF} \alpha \), with \(\alpha \in {\textsf {LTL{+}P} _\textsf {P} }\,\), and assumptions/guarantees, in the form of a logical implication.
Formulas of the logic GR-EBR are defined as follows.
Definition 16
(The logicGR-EBR ) The logic GR-EBR consists of all and only the formulas of the following form:
where \(m,n \in \mathbb {N}\), \(\psi _{ebr}^1,\psi _{ebr}^2 \in {\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} }\,\) and \(\alpha _{i}, \beta _{j} \in {\textsf {LTL{+}P} _\textsf {P} }\,\), for all \(i,j \in \mathbb {N}\).
In order to show the expressive power and naturalness of GR-EBR , we give an example of a meaningful specification that can be formulated in it. More precisely, we take an example that was originally proposed in [9], and we extend it with fairness conditions, assumptions, and guarantees.
Let us consider an arbiter that, given a request from a client i, with \(i \in \{1,\dots ,n\}\), assigns it a grant in such a way to guarantee the following properties: (1) the grant is assigned at most k time units after the request is issued, for some \(k > n\) (bounded response); (2) the arbiter can assign a grant to at most one client at a time (mutual exclusion). The (conjunction of the) two requirements are the guarantees for the controller. The assumptions for the environment are the following: (1) initially, there are no requests; (2) if a client issues a request at time i, then it cannot issue a new request until time \(i+k+1\); (3) each client issues infinitely many requests.
Let us now show how to specify the expected behavior of the arbiter by means of a GR-EBR formula. First of all, we model the requests coming from the n clients with n (uncontrollable) variables \(r_1, \dots , r_n\). Similarly, the grant for the request \(r_i\) can be modeled with a (controllable) variable \(g_i\), for each \(i \in \{1,\dots ,n\}\). The assumption for the environment are expressed by the formula \(\phi _e\), which is defined as follows:
The overall specification is the GR-EBR formula \(\phi _e \rightarrow \phi _c\). The corresponding GR(1) specification is obtained by substituting the subformulas \(r_i \rightarrow \textsf {G} ^{[1,k]} \lnot r_i\) and \(r_i \rightarrow \textsf {F} ^{[0,k]} g_i\) with the equivalent pure past one \(\textsf {Y} ^{k+1} r_i \rightarrow \textsf {H} ^{[1,k]} \lnot r_i\) and \(\textsf {Y} ^{k+1} r_i \rightarrow \textsf {O} ^{[1,k]} g_i\), respectively, where \(\textsf {Y} ^k\), \(\textsf {H} ^{[0,k]}\), and \(\textsf {O} ^{[0,k]}\) are the past operators specular to \(\textsf {X} ^k\), \(\textsf {G} ^{[0,k]}\), and \(\textsf {F} ^{[0,k]}\), respectively.
4 Expressiveness of GR-EBR
In this section, we study the expressiveness of GR-EBR . As a preliminary step, we work out the case of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , on which GR-EBR is based.
We first prove that \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) is expressively complete with respect to the safety fragment of LTL+P . Moreover, we show that past temporal operators, which play a crucial role in the proof of the expressive completeness of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , are really necessary: we prove that \(\textsf {LTL} _\textsf {EBR} \) , that is, \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) devoid of past temporal operator, is strictly less expressive than \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) .
Then, we investigate the expressiveness of GR-EBR and we prove that:
1.
it is strictly more expressive than \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , and thus it can express all safety properties definable in LTL+P and beyond;
2.
it is expressively equivalent to GR(1) .
All the proofs which are not reported in the main body of the paper can be found in the appendix (Sect. A).
4.1 Expressiveness of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \)
In this part, we study the expressiveness of the \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) logic. In particular, we compare the set of languages definable in \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) with the set of safety languages expressible in LTL+P , and prove that the two sets are equal, that is \(\llbracket {\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} }\,\rrbracket = \llbracket \textsf {LTL} \,\rrbracket \cap \textsf {SAFETY} \,\). Consequently (see Theorem 2), \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) and Safety-LTL are expressively equivalent (i.e., \(\llbracket {\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} }\,\rrbracket = \llbracket \textsf {Safety} {\text{- }}\textsf {LTL} \,\,\rrbracket \)).
First we recall the normal-form theorem stated in Theorem 1, establishing that \(\llbracket \textsf {LTL} \,\rrbracket \cap \textsf {SAFETY} \,= \llbracket \textsf {G} \alpha \rrbracket \). Proving that \(\llbracket {\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} }\,\rrbracket = \llbracket \textsf {LTL} \,\rrbracket \cap \textsf {SAFETY} \,\) is straightforward. In [26], Sistla proved that any fragment of LTL+P with only \(\textsf {X} \), \(\textsf {R} \), and \(\textsf {G} \) as future temporal modalities defines only safety properties, and thus is a safety fragment of LTL+P . Since \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) -formulas contain only universal (future) temporal operators, it follows that \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) is a safety fragment of LTL+P (this corresponds to the left-to-right direction). For the right-to-left direction it suffices to show that the normal form \(\textsf {G} \alpha \) is syntactically definable in \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) (i.e., \(\textsf {G} \alpha \in {\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} }\,\) and thus also \(\mathcal {L}(\textsf {G} \alpha ) \in \llbracket {\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} }\,\rrbracket \), for any \(\alpha \in {\textsf {LTL{+}P} _\textsf {P} }\,\)).
Although we proved the expressive equivalence between \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) and \(\textsf {G} \alpha \), we note that \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) offers a more natural language for safety properties than the \(\textsf {G} \alpha \) fragment. Consider for example the following property, expressed in natural language: either \(p_3\) holds forever, or there exists two time points \(t^\prime \le t\) such that (i) \(p_1\) holds in t, (ii) \(p_2\) holds in \(t^\prime \), and (iii) \(p_2\) holds from time point 0 to t. The property can be easily formalized in \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) by the formula \({p_1 \textsf {R} (p_2 \textsf {R} p_3)}\). The equivalent formula in the \(\textsf {G} \alpha \) fragment is \(\textsf {G(H} (p_3) \vee \textsf {O} (p_2 \wedge \textsf {O} (p_1) \wedge \textsf {H} (p_3)))\), which is arguably more intricate.
4.3 Comparison with Safety-LTL
Safety-LTL is the fragment of LTL (thus with only future temporal modalities) containing all and only the LTL -formulas that, when in negated normal form, do not contain any until or eventually operator. From Theorems 2 and 8, it immediately follows that \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) and Safety-LTL are expressively equivalent, namely \(\llbracket {\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} }\,\rrbracket = \llbracket \textsf {Safety} {\text{- }}\textsf {LTL} \,\,\rrbracket \).
Unlike \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , Safety-LTL does not impose any syntactic restriction on the nesting of the logical operators; as a matter of fact, \(\textsf {G} (p_1 \vee \textsf {G} p_2)\) belongs to the syntax of Safety-LTL but not to the syntax of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , even though \(\textsf {G} (p_1 \vee \textsf {G} p_2) \equiv \textsf {G} (\lnot p_2 \rightarrow \textsf {H} p_1) \in {\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} }\,\). The restrictions on the syntax of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) are due to algorithmic aspects: each layer of the syntax of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) (recall Def. 3) corresponds to a step of the algorithm for the construction of deterministic and symbolic automata starting from \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) -formulas [9]. As a matter of fact, in practice, \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) has shown to avoid an exponential blowup in time with respect to known algorithms for automata contruction for safety specifications [9]. Last but not least, the realizability problem of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) is EXPTIME -complete [9], as opposed to the realizability of LTL+P , which is 2EXPTIME-complete [5, 6]. Consider now \(\textsf {LTL} _\textsf {EBR} \) , which is the fragment of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) devoid of past operators (Def. 5). Since each formula of \(\textsf {LTL} _\textsf {EBR} \) syntactically belongs to Safety-LTL , it immediately follows that \(\llbracket {\textsf {LTL} _\textsf {EBR} }\,\rrbracket \subseteq \llbracket \textsf {Safety} {\text{- }}\textsf {LTL} \,\,\rrbracket \). In Sect. 4.4, we will prove that the converse direction does not hold, that is \(\textsf {LTL} _\textsf {EBR} \) is strictly less expressive than \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) and Safety-LTL .
4.4 Expressiveness of \(\textsf {LTL} _\textsf {EBR} \)
In Sect. 4.1, we have proved that the following equivalences hold:
In particular, thanks to the use of the pure past layer (recall Def. 5), \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) can easily capture the whole class of \(\llbracket \textsf {G} \alpha \rrbracket \), and thus the whole class of \(\llbracket \textsf {LTL} \,\rrbracket \cap \textsf {SAFETY} \,\). However, one may wonder whether the pure past layer is really necessary, or whether the class \(\llbracket \textsf {G} \alpha \rrbracket \) can be expressed in \(\textsf {LTL} _\textsf {EBR} \) without the use of past operators.
Recall from Def. 5 that \(\textsf {LTL} _\textsf {EBR} \) is defined as the fragment of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) devoid of the pure past layer. In this part, we prove that the removal of past operators from \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) results into a loss of expressive power, namely:
This result proves that past modalities, although being not important for the expressiveness of full LTL (since \(\llbracket \textsf {LTL} \,\rrbracket = \llbracket \textsf {LTL{+}P} \,\rrbracket \) [16‐18]), can play a crucial role for the expressive power of fragments of LTL , like, for instance, \(\textsf {LTL} _\textsf {EBR} \) .
4.4.1 The general idea
We will prove Eq. (1) by showing that \(\llbracket {\textsf {LTL} _\textsf {EBR} }\,\rrbracket \subsetneq \llbracket \textsf {Safety} {\text{- }}\textsf {LTL} \,\,\rrbracket \). The result in Eq. (1) follows from the fact that \(\llbracket \textsf {Safety} {\text{- }}\textsf {LTL} \,\,\rrbracket = \llbracket {\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} }\,\rrbracket \). We shall prove that the language of the Safety-LTL -formula \(\varphi _{\textsf {G} }{:=}\textsf {G} (p_1 \vee \textsf {G} (p_2))\) cannot be expressed by any \(\textsf {LTL} _\textsf {EBR} \) -formula. The formula \(\varphi _{\textsf {G} }\) belongs syntactically to Safety-LTL , and thus \(\mathcal {L}(\varphi _{\textsf {G} }) \in \llbracket \textsf {Safety} {\text{- }}\textsf {LTL} \,\,\rrbracket \). We also note that \(\varphi _{\textsf {G} }\) can be expressed in \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) . Indeed, it holds that:
Since \(\textsf {G} (\lnot p_2 \rightarrow \textsf {H} (p_1)) \in {\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} }\,\), it holds that \(\mathcal {L}(\varphi _{\textsf {G} }) \in \llbracket {\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} }\,\rrbracket \). It is worth noticing the following points: (i) \(\textsf {G} (\lnot p_2 \rightarrow \textsf {H} (p_1))\) is of the form \(\textsf {G} \alpha \), where \(\alpha \in {\textsf {LTL{+}P} _\textsf {P} }\,\) (\(\alpha \) is a pure past formula); (ii) the formula \(\varphi _{\textsf {G} }\) is equivalent to \(\textsf {G} (p_2) \vee ((\textsf {X G} p_2) \textsf {R} p_1)\), but the latter formula does not syntactically belong to \(\textsf {LTL} _\textsf {EBR} \) nor to \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , due to the restriction that forces the leftmost argument of any release operator to contain no universal temporal operators (i.e., \(\textsf {R} \) and \(\textsf {G} \)).
The proof of the undefinability of \(\varphi _{\textsf {G} }\) is based on the fact that all formulas of \(\textsf {LTL} _\textsf {EBR} \) can constrain, for any time point i in an infinite state sequence, only a bounded prefix before (or interval around) i.
Consider again the formula \(\varphi _{\textsf {G} }{:=}\textsf {G} (p_1 \vee \textsf {G} (p_2))\). The language \(\mathcal {L}(\varphi _{\textsf {G} })\) is expressed by the \(\omega \)-regular expression \((\{p_1\})^\omega + (\{p_1\})^*\cdot (\{p_2\})^\omega \). Written in natural language, each model of \(\varphi _{\textsf {G} }\) cannot contain a position in which \(\lnot p_2\) holds preceded by a position in which \(\lnot p_1\) holds.
Remark 1
Let \(\sigma \subseteq (2^\Sigma )^\omega \) be a state sequence. It holds that:
Let \(^{i,k}\sigma ^j\) be the state sequence such that at time points i and k it holds \(p_1 \wedge \lnot p_2\), at time point j it holds \(\lnot p_1 \wedge p_2\), and for all the other time points \(p_1 \wedge p_2\) holds (a formal definition of \(^{i,k}\sigma ^j\) will be given later). The membership of \(^{i,k}\sigma ^j\) to \(\mathcal {L}(\varphi _{\textsf {G} })\) depends on the value of the three indices i, j and k, as follows.
Remark 2
If \(i<j\) and \(k<j\), then \(^{i,k}\sigma ^j \models \varphi _{\textsf {G} }\). Conversely, if \(i \ge j\) or \(k \ge j\), then \(^{i,k}\sigma ^j \not \models \varphi _{\textsf {G} }\).
As we will see, given a generic formula \(\psi \in {\textsf {LTL} _\textsf {EBR} }\,\), one can always find some values for the indices i, j and k such that (a) j is chosen sufficiently greater than i; (b) k is chosen sufficiently greater than j; (c) \(\psi \) is not able to distinguish the state sequence \(^{i,i}\sigma ^j\) from \(^{i,k}\sigma ^j\). Since, by Remark 2, \(^{i,i}\sigma ^j \in \mathcal {L}(\varphi _{\textsf {G} })\) but \(^{i,k}\sigma ^j \not \in \mathcal {L}(\varphi _{\textsf {G} })\), this proves the undefinability of \(\varphi _{\textsf {G} }\) in \(\textsf {LTL} _\textsf {EBR} \) . The rationale is that the \(\textsf {LTL} _\textsf {EBR} \) logic combines bounded future formulas (i.e., formulas obtained by a Boolean combination of propositional atoms and \(\textsf {X} \) operators) and universal temporal operators (i.e., \(\textsf {G} \) and \(\textsf {R} \)). This implies the fact that, for a generic model \(\sigma \) of an \(\textsf {LTL} _\textsf {EBR} \) -formula \(\psi \), at each time point\(i \ge 0\) of \(\sigma \) (this corresponds to the universal temporal operators) only a finite and bounded suffix after i (this corresponds to the \(\textsf {LTL{+}P} _\textsf {BF} \) -formulas) can be constrained by \(\psi \) (this can be thought of as a sort of bounded memory property of this logic). Equivalently, this means that each \(\textsf {LTL} _\textsf {EBR} \) -formula is not able to constrain any finite but arbitrarly long (unbounded) prefix of a state sequence, contrary, for instance, to the case of the formula \(\textsf {G} (\lnot p_2 \rightarrow \textsf {H} (p_1))\) (that is equivalent to \(\varphi _{\textsf {G} }\), see Eq. (2)).
4.4.2 The normal form
The limitation of \(\textsf {LTL} _\textsf {EBR} \) -formulas mentioned before is more evident in the normal form for the \(\textsf {LTL} _\textsf {EBR} \) logic, that we will define in this part. We first give some preliminary definitions. We define Bounded Past\(\textsf {LTL{+}P} _\textsf {P} \) (\(\textsf {LTL{+}P} _\textsf {BP} \) , for short) as the set of all and only the \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) formulas that are a Boolean combination of propositional atoms and yesterday operators (\(\textsf {Y} \)). We use the shortcut \(\textsf {Y} ^n\psi \) for denoting \(\psi \) is \(n=0\), and \(\textsf {Y Y} ^{n-1} \psi \) otherwise. We use also the shortcut \(\psi _1 \textsf {S} ^{[a,b]} \psi _2\) for denoting the formula \(\bigvee _{i=a}^{b} ( \textsf {Y} ^i (\psi _2) \wedge \bigwedge _{j=0}^{i-1} \textsf {Y} ^j (\psi _1))\). Given a formula \(\alpha \in {\textsf {LTL{+}P} _\textsf {BP} }\,\), we define its temporal depth, denoted as \(D(\alpha )\), as follows:
For each \(\alpha \in {\textsf {LTL{+}P} _\textsf {BP} }\,\), the language \(\mathcal {L}^{<\omega }(\alpha )\) consists only of words of length at most \(D(\alpha )+1\). Recall from Sect. 2 that, given an infinite state sequence \(\sigma = \langle \sigma _0,\sigma _1,\dots \rangle \) and some \(n \ge 0\), \(\sigma _{[n-d,n]}\) is the interval of \(\sigma \) of length at mostd ending at index n. The crucial property of \(\textsf {LTL{+}P} _\textsf {BP} \) -formulas, that can be shown with a simple induction, is that their truth over a state sequence \(\sigma \) can be checked by considering only a finite and bounded interval of \(\sigma \), whose length depends on the temporal depth of the formula. This is summarized by the following remark.
Remark 3
For any \(\alpha \in {\textsf {LTL{+}P} _\textsf {BP} }\,\), with temporal depth \(d=D(\alpha )\), and for any \(n \ge 0\), it holds that \(\sigma ,n \models \alpha \)if and only if\(\sigma _{[n-d,n]} \models \alpha \).
We give now the normal form for \(\textsf {LTL} _\textsf {EBR} \) , and we refer to it as Normal-\(\textsf {LTL} _\textsf {EBR} \) . The normal form of \(\textsf {LTL} _\textsf {EBR} \) forces any universal unbounded operator, like globally or release, to contain only \(\textsf {LTL{+}P} _\textsf {BP} \) -formulas. Formally, we define Normal-\(\textsf {LTL} _\textsf {EBR} \) as the normal form described in Def. 4 but such that each \(\alpha _i,\beta _i\) is a bounded pastLTL formula. For sake of clarity, we write here below the full definition.
Definition 17
(Normal Form of\(\textsf {LTL} _\textsf {EBR} \) ) The normal form of \(\textsf {LTL} _\textsf {EBR} \) is the set of all and only the formulas of the following type:
where each \(\alpha _i,\beta _i \in {\textsf {LTL{+}P} _\textsf {BP} }\,\), \(\otimes \in \{\wedge , \vee \}\), and \(i,j,k,h \in \mathbb {N}\).
By applying the same transformation from \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) to its normal form given in [9], one obtain the following lemma.
The normal form of \(\textsf {LTL} _\textsf {EBR} \) makes it easier to prove Eq. (1). Take, e.g., the formula \(\textsf {XXG} (p \vee \textsf {Y} p \vee \textsf {YY} p)\), that belongs to Normal-\(\textsf {LTL} _\textsf {EBR} \) . It is clear that, at each time point, this formula can constrain only the interval consisting of the current state and its two previous states (in fact its temporal depth is 3).
4.4.3 The main proof
We now show that the formula \(\varphi _{\textsf {G} }\) is not definable in the logic Normal-\(\textsf {LTL} _\textsf {EBR} \) . Undefinability in \(\textsf {LTL} _\textsf {EBR} \) follows from Lemma 4.
Given three indices \(i,j,k \in \mathbb {N}\) such that \(i \not = j\) and \(k \not = j\), we formally define the state sequence \(^{i,k}\sigma ^j = \langle {}^{i,k}\sigma ^j_0, \ {}^{i,k}\sigma ^j_1,\dots \rangle \) as follows:
The core of the main theorem is based on the fact that any formula of type \(\textsf {G} \alpha \) or \(\alpha \textsf {R} \beta \), where \(\alpha \) and \(\beta \) are bounded past\(\textsf {LTL{+}P} _\textsf {P} \) formulas, is not able to distinguish the state sequence \(^{i,i}\sigma ^j\) with \(i<j\) (which is a model of \(\varphi _{\textsf {G} }\)) from \(^{i,k}\sigma ^j\) with \(k>j\) (which is not a model of \(\varphi _{\textsf {G} }\)), for sufficiently large values of i, j and k. The choice for the values of the three indices is based on the values of the temporal depth of \(\alpha \) and \(\beta \). Since the globally operator is a special case of the release operator, that is \(\textsf {G} \alpha \equiv \bot \textsf {R} \alpha \), it suffices to prove the property for formulas of type \(\alpha \textsf {R} \beta \). We first prove two fundamental properties that show that, for any interval of \(^{i,i}\sigma ^j\) of length at most d (for any \(d \in \mathbb {N}\)), we can find the exact same interval in \(^{i,k}\sigma ^j\), and vice versa. The two properties are proved by the following lemma. Figure 2 shows the idea of this correspondence.
Fig. 2
Graphical exemplification of Lemma 5
×
Lemma 5
Let \(d \in \mathbb {N}\). For all \(i \ge d\), for all \(j \ge i+d\), and for all \(k \ge j+d\), it holds that:
Lemma 5 allows to prove that the state sequences \({}^{i,i}\sigma ^{j}\) and \({}^{i,k}\sigma ^{j}\) are indistinguishable for each formula of type \(\alpha \textsf {R} \beta \) (and, consequently, of type \(\textsf {G} \alpha \)), with \(\alpha ,\beta \in {\textsf {LTL{+}P} _\textsf {BP} }\,\).
Lemma 6
Let \(\alpha ,\beta \in {\textsf {LTL{+}P} _\textsf {BP} }\,\), and let \(d = \max \{D(\alpha ),D(\beta )\}\) be the maximum between the temporal depths of \(\alpha \) and \(\beta \). It holds that \(\ {}^{i,i}\sigma ^j \models \alpha \textsf {R} \beta \) iff \(\ {}^{i,k}\sigma ^j \models \alpha \textsf {R} \beta \), for all \(i \ge d\), for all \(j \ge i+d\), and for all \(k \ge j+d\).
By using Lemma 6 as the proof for the base case, we prove by induction on the structure of the formula that any formula in Normal-\(\textsf {LTL} _\textsf {EBR} \) is not able to distinguish the state sequences \({}^{i,i}\sigma ^j\) and \({}^{i,k}\sigma ^j\) for sufficiently large values of i, j, k. In the following, given a formula \(\psi \in \textsf {Normal} {\text{- }}{\textsf {LTL} _\textsf {EBR} }\,\,\), we will denote with \(m_\psi \) the maximum number of nested next operators in \(\psi \), and with \(d_\psi \) the maximum temporal depth between all its \(\textsf {LTL{+}P} _\textsf {BP} \) -subformulas.
Lemma 7
Let \(\psi \in \textsf {Normal} {\text{- }}{\textsf {LTL} _\textsf {EBR} }\,\,\). It holds that \({}^{i,i}\sigma ^j \models \psi \) iff \({}^{i,k}\sigma ^j \models \psi \), for all \(i \ge m_\psi + d_\psi \), for all \(j \ge i+d_\psi \), and for all \(k \ge j+d_\psi \).
Thanks to Lemma 7, it is simple to prove the undefinability of \(\textsf {G} (p_1 \vee \textsf {G} (p_2))\) in \(\textsf {LTL} _\textsf {EBR} \) , establishing that \(\textsf {LTL} _\textsf {EBR} \) is strictly less expressive than Safety-LTL .
Consider the formula \(\varphi _{\textsf {G} }{:=}\textsf {G} (p_1 \vee \textsf {G} (p_2))\). We prove that there does not exists a formula \(\psi \in {\textsf {LTL} _\textsf {EBR} }\,\) such that \(\mathcal {L}(\psi ) = \mathcal {L}(\varphi _{\textsf {G} })\). We proceed by contradiction. Suppose that there exists a formula \(\psi \in {\textsf {LTL} _\textsf {EBR} }\,\) such that \(\mathcal {L}(\psi ) = \mathcal {L}(\varphi _{\textsf {G} })\). By Lemma 4, there exists a formula \(\psi ^{\prime } \in \textsf {Normal} {\text{- }}{\textsf {LTL} _\textsf {EBR} }\,\,\) such that \(\mathcal {L}(\psi ) = \mathcal {L}(\psi ^\prime )\). Let \(m_{\psi ^\prime }\) be the maximum number of nested next operators in \(\psi ^\prime \), and let \(d_{\psi ^\prime }\) be the maximum temporal depth between all the \(\textsf {LTL{+}P} _\textsf {BP} \) -subformulas in \(\psi ^\prime \). Let k, i and j be three indices such that: (i) \(i \ge m_{\psi ^\prime } + d_{\psi ^\prime }\); (ii) \(j \ge i + d_{\psi ^\prime }\); (iii) and \(k \ge j + d_{\psi ^\prime }\). Consider the two state sequences \({}^{i,i}\sigma ^j\) and \({}^{i,k}\sigma ^j\). By Lemma 7, \({}^{i,i}\sigma ^j \in \mathcal {L}(\psi ^\prime )\) if and only if \({}^{i,k}\sigma ^j \in \mathcal {L}(\psi ^\prime )\), that is \({}^{i,i}\sigma ^j \in \mathcal {L}(\varphi _{\textsf {G} })\) if and only if \({}^{i,k}\sigma ^j \in \mathcal {L}(\varphi _{\textsf {G} })\). Since it holds that \({}^{i,i}\sigma ^j \in \mathcal {L}(\varphi _{\textsf {G} })\) but \({}^{i,k}\sigma ^j \not \in \mathcal {L}(\varphi _{\textsf {G} })\), this is clearly a contradiction. \(\square \)
We are now ready to study the expressiveness of GR-EBR by comparing it with (i) \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , (ii) Manna and Pnueli’s temporal hierarchy, and (iii) GR(1) .
4.6 Comparison with
\(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) and the (co-)safety LTL fragment
We start by comparing GR-EBR with \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) . Each \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) formula \(\phi \) is a GR-EBR formula as well. In fact, the formula \(\phi \) is equivalent to \({(\top \wedge \top ) \rightarrow (\phi \wedge \top )}\) which belongs to GR-EBR , thus: \({\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} }\,\subseteq \textsf {GR} {\text{- }}\textsf {EBR} \,\) and of course \(\llbracket {\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} }\,\rrbracket \subseteq \llbracket \textsf {GR} {\text{- }}\textsf {EBR} \,\rrbracket \).
From Theorem 8, it follows that any safety language definable in LTL is definable in GR-EBR as well. In addition, GR-EBR is strictly more expressive than \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , since the former can express also non-safety properties, like \(\textsf {G} p \rightarrow \textsf {G} q\), and thus:
Thanks to the implication in the syntax of GR-EBR , we can also define co-safety properties. Actually, it turns out that we can express all the LTL -definable co-safety properties. Take a language \(\mathcal {L}\in \llbracket \textsf {LTL} \,\rrbracket \cap \textsf {coSAFETY} \,\). By Theorem 1, \(\mathcal {L}= \mathcal {L}(\textsf {F} \alpha )\), for a given formula \(\alpha \in {\textsf {LTL{+}P} _\textsf {P} }\,\). Now, any formula of type \(\textsf {F} \alpha \) (with \(\alpha \in {\textsf {LTL{+}P} _\textsf {P} }\,\)) can be easily defined with the syntax of GR-EBR by the formula \((\textsf {G} \lnot \alpha ) \rightarrow \bot \). Therefore:
We consider the Reactivity(N) class (R(N) ) of the Temporal Hierarchy (see Sect. 2.4) for \(N=1\). We recall that the resulting class, R(1) (i.e., Reactivity(1)), comprises all and only the formulas of type:
with \(\alpha ,\beta \in {\textsf {LTL{+}P} _\textsf {P} }\,\). Since any R(1) -formula is syntactically also a GR(1) -formula, it is straightforward to see that GR-EBR is at least as expressive as R(1) .
\(\alpha _T, \beta _T\) are \(\textsf {LTL{+}P} _\textsf {BF} \) formulas where modality \(\textsf {X} \) can only occur in a non-nested form, and
(iii)
\(\alpha _i,\beta _j\) are \({\textsf {LTL{+}P} _\textsf {P} }\,\) formulas, for all \(i\in \{1,\dots ,m\}\) and \(j\in \{1,\dots ,n\}\), for some \(m,n \in \mathbb {N}\).
We prove that GR-EBR is expressively equivalent to GR(1) .
We first prove that \(\llbracket \textsf {GR} {\text{- }}\textsf {EBR} \,\rrbracket \subseteq \llbracket \textsf {GR(1)} \,\rrbracket \). Let \(\phi \) be a formula of GR-EBR . By definition, \(\phi \) is of this type:
By Theorem 8, there exists two \(\textsf {LTL{+}P} _\textsf {P} \) formulas \(\alpha _1,\alpha _2\) such that \(\psi _{ebr}^1 \equiv \textsf {G} \alpha _1\) and \(\psi _{ebr}^2 \equiv \textsf {G} \alpha _2\). Therefore, \(\phi \) is equivalent to:
Without loss of generality, consider the left-hand side of the implication (the argument works in the very same way for the right-hand side).
By applying the pastification method [9, 35] to \(\alpha _T\), we lift the occurrences of the next operator \(\textsf {X} \) in \(\alpha _T\) to the top level and obtain an equivalent formula of the form \(\textsf {X} \alpha _T^\prime \) such that \(\alpha _T^\prime \in {\textsf {LTL{+}P} _\textsf {P} }\,\). Now, since, for any state sequence \(\sigma \), it holds that \(\sigma ,i \models \textsf {Y} \top \) if and only if \(i>0\), that is, i is not the initial state, it holds that \(\textsf {G} (\textsf {X} \alpha _T^\prime )\) is equivalent to \(\textsf {G} (\textsf {Y} \top \rightarrow \alpha _T^\prime )\), which is of the desired form \(\textsf {G} \alpha ^\prime \) with \(\alpha ^\prime {:=}\textsf {Y} \top \rightarrow \alpha _T^\prime \).
Therefore, we obtain that any GR(1) formula can be translated into an equivalent one of the form:
where \(\alpha ^\prime ,\beta ^\prime \in {\textsf {LTL{+}P} _\textsf {P} }\,\). Since both \(\alpha _I \wedge \textsf {G} (\alpha ^\prime )\) and \(\beta _I \wedge \textsf {G} ( \beta ^\prime )\) syntactically belong to \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , this proves that the whole formula belongs to GR-EBR and thus \(\llbracket \textsf {GR(1)} \,\rrbracket \subseteq \llbracket \textsf {GR} {\text{- }}\textsf {EBR} \,\rrbracket \). \(\square \)
Figure 3 shows the comparison between the expressive power \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , \(\textsf {LTL} _\textsf {EBR} \) and GR-EBR and the other fragments that we considered.
Fig. 3
Comparison of the expressive power of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , \(\textsf {LTL} _\textsf {EBR} \) and GR-EBR . For ease of exposition, we highlighted the rectangles corresponding to \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , \(\textsf {LTL} _\textsf {EBR} \) and GR-EBR with thick borders
Fig. 4
Low-level view of the procedure for the realizability of GR-EBR formulas
×
×
Our goal is to solve the realizability problem for GR-EBR specifications by reducing it to realizability subproblems for safety specifications. The reduction to safety, which we will give in Sect. 5, generates a safety formula for each integer k, in such a way to guarantee the following important properties: (i) soundness, ensuring that the realizability of the \(k^{th}\) subproblem implies the realizability of the starting formula, and (ii) completeness, establishing the existence of an upper bound \(\mu \) such that the unrealizability of all the \(k^{th}\) subproblems with \(k \le \mu \) implies the unrealizability of the starting formula. In Sect. 5, we describe a symbolic algorithm that performs a safety reduction for the realizability problem from GR-EBR specifications. In order to prove completeness of such algorithm, in Sect. 6 we introduce a general framework for deriving (sound and) complete safety reductions for arbitrary fragments of LTL , and we instantiate this framework to the GR-EBR case.
5 GR-EBR synthesis: the algorithm
In this section, we describe the algorithm for solving realizability of GR-EBR specifications.
The procedure consists of three steps. Firstly, we build the product between the two symbolic safety automata for the safety parts of both assumptions and guarantees, and we define a GR(1) accepting condition for it in order to maintain the language-equivalence with the original formula. The second step consists of a so-called degeneralization, that, by using deterministic monitors, turns the GR(1) accepting condition into a Reactivity(1) (R(1) , for short) condition. The third and last step, that is the core of the procedure, reduces the realizability problem over the above automaton to a sequence of safety games (Def. 15), that is, realizability problems over safety (and symbolic) automata \(\mathcal {A}_{ safe }^{\textrm{k}}\), one for each index \(k \in \mathbb {N}\). The structure of the full procedure is depicted in Fig. 4.
Since, in the worst case, the upperbound given by the safety reduction is doubly exponential in the length of the formula, in practice it is useful to use our algorithm in parallel with another one that checks for the unrealizability of the specification. The first that terminates stops the other and, thus, the entire procedure, as summarized in Fig. 5. We remark that we cannot check the unrealizability of \(\phi \) by solving the dualized game (i.e., looking for a Moore-type strategy of Environment) for \(\lnot \phi \), because GR-EBR and \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) are not closed under complementation.
Fig. 5
High-level view of our procedure for the realizability of GR-EBR formulas
×
Finally, note that, as for now, there is no incrementality between an iteration and the next one, because of the lack of incremental safety synthesizers. The only point that we save between one iteration and the next one is the construction of the two symbolic safety automata, which is performed only once during the procedure.
5.1 Construction of the automaton with a GR(1) condition
In this part, we describe the first step of the algorithm. Starting from a GR-EBR formula \(\phi {:=}(\phi _{ebr}^1 \wedge \bigwedge _{i=1}^{m} \textsf {G F} \alpha _i) \rightarrow (\phi _{ebr}^2 \wedge \bigwedge _{j=1}^{n} \textsf {G F} \beta _j)\), the objective is to obtain an automaton \(\mathcal {A}\) such that: (i) it has a GR(1) accepting condition, and (ii) it recognizes the same language of \(\phi \), i.e., \(\mathcal {L}(\phi ) = \mathcal {L}(\mathcal {A})\). In order to do that, we first build the two symbolic safety automata for the safety parts of both the assumptions and the guarantees, that is for \(\phi _{ebr}^1\) and \(\phi _{ebr}^2\). Since by definition both are \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) formulas, we use the transformation described in [9], to which the reader is referred for more details.
From now on, let \(\mathcal {A}(\phi _{ebr}^1)\) and \(\mathcal {A}(\phi _{ebr}^2)\) be the automata for \(\phi _{ebr}^1\) and \(\phi _{ebr}^2\), respectively. Let \(\mathcal {A}_{ ebr }\) be the product automaton \(\mathcal {A}(\phi _{ebr}^{1}) \times \mathcal {A}(\phi _{ebr}^{2})\). The question is how to set the acceptance condition of \(\mathcal {A}_{ ebr }\) such that the conditions (i) and (ii) above are fulfilled. We answer this question by examining how the automata \(\mathcal {A}(\phi _{ebr}^{1})\) and \(\mathcal {A}(\phi _{ebr}^{2})\) are made internally. Take for example the formula \(\textsf {G} p\) (for some atomic proposition \(p \in \Sigma \)). The safety automaton corresponding to this formula (but the same holds for all \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) formulas) comprises an error bit as one of its state variables, let us call it error, which is initially set to be false (when the automaton has not start to read any letter of the input word). The transition function for error is deterministic and updates error to true if \(\lnot p\) holds in the current state, or keeps its value otherwise. The set of safe states comprises all and only those states in which error is false. In a symbolic setting, this is expressed by the formula \(\textsf {G} \lnot \texttt {error}\). In this way, p is forced to hold constantly in all (and only) the words accepted by the automaton.
A crucial property of each error bit is monotonicity: once \(\texttt {error}\) is set to \(\texttt {true}\), it can never be set to \(\texttt {false}\) again. Formally, given a run \(\tau \) of the automaton, it holds that, if there exists \(i \ge 0\) such that \(\tau (i) \models \texttt {error}\), then \(\tau (j) \models \texttt {error}\), for all \(j \ge i\). Monotonicity of error bits allows us to express an accepting condition of type \(\textsf {G} \lnot \texttt {error}\) in terms of \(\textsf {G F} \lnot \texttt {error}\) (which is of the GR(1) type) by maintaining the equivalence.
Lemma 1
\(\textsf {G} \lnot \texttt {error} \equiv \textsf {G F} \lnot \texttt {error}\), under the assumption that \(\texttt {error}\) is monotone.
Proof
Consider a run \(\tau \) of an automaton with an accepting condition of the type \(\textsf {G} \lnot \texttt {error}\). If \(\tau \models \textsf {G} \lnot \texttt {error}\) then of course \(\tau \models \textsf {G F} \lnot \texttt {error}\). Suppose now that \(\tau \models \textsf {G F} \lnot \texttt {error}\). If by contradiction we suppose that \(\tau \not \models \textsf {G} \lnot \texttt {error}\), we have that there exists an \(i \ge 0\) such that \(\tau (i) \models \texttt {error}\). By the monotonicity property, this would mean that also \(\tau (j) \models \texttt {error}\), for all \(j \ge i\), that is \(\tau \models \textsf {F G} \texttt {error}\), but this a contradiction with our hypothesis. Therefore, we proved that changing the acceptance condition of an automaton from a \(\textsf {G} \lnot \texttt {error}\) to \(\textsf {G F} \lnot \texttt {error}\) maintains the equivalence. \(\square \)
Let \(\texttt {error}_1\) and \(\texttt {error}_2\) be the error bits of \(\mathcal {A}(\phi _{ebr}^{1})\) and \(\mathcal {A}(\phi _{ebr}^{2})\), respectively. Let \(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}}\) be the automaton obtained from \(\mathcal {A}_{ ebr }\) by replacing its acceptance condition with the following GR(1) condition:
The intuition is that \(\texttt {error}_1\) and \(\texttt {error}_2\) keep track of the safety parts of \(\phi \), that is \(\phi _{ebr}^{1}\) and \(\phi _{ebr}^{2}\). The following lemma proves the equivalence between \(\phi \) and \(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}}\).
Lemma 2
Let \(\phi \) be an GR-EBR formula. It holds that \(\mathcal {L}(\phi ) = \mathcal {L}(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}})\).
Proof
Let \(\phi \in \textsf {GR} {\text{- }}\textsf {EBR} \,\). \(\phi \) is of the following form:
By the theorems proved in [9], it holds that \(\mathcal {L}(\phi _{ebr}^{1}) = \mathcal {L}(\mathcal {A}(\phi _{ebr}^{1}))\) and \(\mathcal {L}(\phi _{ebr}^{2}) = \mathcal {L}(\mathcal {A}(\phi _{ebr}^{2}))\).
Consider first the left-to-right direction. Let \(\sigma \in \mathcal {L}(\phi )\). We prove that \(\sigma \in \mathcal {L}(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}})\). Each \(\sigma \in \mathcal {L}(\phi )\) is such that: a. either \(\sigma \models \lnot \phi _{ebr}^{1} \vee \lnot (\bigwedge _{i=1}^{m} \textsf {G F} \alpha _i)\), b. or \(\sigma \models \phi _{ebr}^{2} \wedge \bigwedge _{j=1}^{n} \textsf {G F} \beta _j\) Recall that \(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}}\) is defined as the product automaton \(\mathcal {A}(\phi _{ebr}^{1}) \times \mathcal {A}(\phi _{ebr}^{2})\) with the acceptance condition \(\alpha \) defined as \((\textsf {G F} \lnot \texttt {error}_1 \wedge \bigwedge _{i=1}^{m} \textsf {G F} \alpha _i) \rightarrow (\textsf {G F} \lnot \texttt {error}_1 \wedge \bigwedge _{j=1}^{n} \textsf {G F} \beta _j)\).
Consider case a. If \(\sigma \models \lnot \phi _{ebr}^{1} \vee \lnot (\bigwedge _{i=1}^{m} \textsf {G F} \alpha _i)\), then the run induced by \(\sigma \) in \(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}}\) is such that at least one of the following two cases hold:
a.1.
either \(\exists i \ge 0\) such that \(\tau (i) \models \texttt {error}_1\), that is \(\tau \models \textsf {F} (\texttt {error}_1)\). In this case, we exploit monotonicity of \(\texttt {error}_1\). Since \(\tau \models \textsf {F} (\texttt {error}_1)\), it also holds that \(\tau \models \textsf {F G} (\texttt {error}_1)\), that is \(\tau \not \models \textsf {G F} (\lnot \texttt {error}_1)\). As a consequence, \(\tau \models \alpha \), where \(\alpha \) is the acceptance condition of \(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}}\), and thus \(\sigma \in \mathcal {L}(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}})\).
a.2.
or \(\tau \models \lnot \bigwedge _{i=1}^{m} \textsf {G F} \alpha _i\). In this case, of course, \(\tau \models \alpha \) (that is, \(\tau \) satisfies the acceptance condition of \(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}}\)), and thus \(\sigma \in \mathcal {L}(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}})\).
Consider now the case b. If \(\sigma \models \phi _{ebr}^{2} \wedge \bigwedge _{j=1}^{n} \textsf {G F} \beta _j\), then \(\sigma \models \phi _{ebr}^{2}\) and \(\sigma \models \bigwedge _{j=1}^{n} \textsf {G F} \beta _j\). Therefore, the run induced by \(\sigma \) in \(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}}\) is such that \(\tau \models \textsf {G} (\lnot \texttt {error}_2) \wedge \bigwedge _{j=1}^{n} \textsf {G F} \beta _j\), that implies that \(\tau \models \textsf {G F} (\lnot \texttt {error}_2) \wedge \bigwedge _{j=1}^{n} \textsf {G F} \beta _j\). Therefore, \(\tau \models \alpha \), and thus \(\sigma \in \mathcal {L}(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}})\). The opposite direction can be proved similarly. \(\square \)
5.2 Optimization
Instead of considering the acceptance condition described in Eq. (3), we propose to repeat the error bits inside each fairness condition.
This may be helpful during the safety game solving, since it creates a redundancy that the solver may exploit during the search. Obviously, this maintains the equivalence.
5.3 Degeneralization
The objective of this part is to transform the GR(1) accepting condition of the automaton \(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}}\), that is of the form \(\bigwedge _{i=1}^{m} \textsf {G F} \alpha _i \rightarrow \bigwedge _{j=1}^{n} \textsf {G F} \beta _j\), into a R(1) accepting condition of the form \(\textsf {G F} \alpha \rightarrow \textsf {G F} \beta \). In this context, we will use the term monitor as a synonym of symbolic deterministic safety automaton (recall Def. 6).
In order to accomplish the task, for each \(\alpha _i\) (resp. for each \(\beta _i\)), we define a monitor \(M_{\alpha _i}\) (resp. \(M_{\beta _i}\)) whose only state variable is set to true when \(\alpha _i\) (resp. \(\beta _i\)) has been read and is reset to false when all the \(\alpha _i\) (resp. \(\beta _i\)) have been read. For this last condition, we define the monitors \(M^{tot}_{\alpha }\) and \(M^{tot}_{\beta }\).
Let \(M_{\alpha _i}\) and \(M^{tot}_{\alpha }\) be the monitors such that (i) their input alphabet is \(2^\Sigma \) (where \(\Sigma \) is the alphabet of the starting GR-EBR formula); (ii) their set of state variables are \(\{m_{\alpha _i}\}\) and \(\{m^{tot}_{\alpha }\}\), respectively; (iii) their set of safe states are their reachable states; and (iv) their transition relations are the following (written in the SMV language [36]).
×
We define \(M_{\beta _j}\) and \(M^{tot}_{\beta }\) in a similar way as \(M_{\alpha _i}\) and \(M^{tot}_{\alpha }\), respectively, but with \(\alpha _i\) substituted with \(\beta _j\) and \(\alpha \) substituted with \(\beta \).
Let \(\mathcal {A}^{\textsf {R(1)} \,}_{\textrm{degen}}\) be the product between \(M_{\alpha _i}\) (for each \(0\le i \le m\)), \(M_{\beta _j}\)(for each \(0\le j \le n\)), \(M^{tot}_{\alpha }\) and \(M^{tot}_{\beta }\), whose accepting condition is the R(1) formula \(\textsf {G F} m^{tot}_{\alpha } \rightarrow \textsf {G F} m^{tot}_{\beta }\). We can prove the following lemma, which states that this step of the algorithm maintains the equivalence.
We prove separately the two directions. Consider first the right-to-left direction. Let \(\sigma \) be an infinite word of \(\mathcal {L}(\mathcal {A}_{ ebr }\times \mathcal {A}^{\textsf {R(1)} \,}_{\textrm{degen}})\). Then \(\sigma \) is a word in \(\mathcal {L}(\mathcal {A}_{ ebr })\). Moreover, \(\sigma \) is a word in \(\mathcal {L}(\mathcal {A}^{\textsf {R(1)} \,}_{\textrm{degen}})\) and thus there exists a run \(\tau \) induced by \(\sigma \) such that \(\tau \models \textsf {G F} m^{tot}_{\alpha } \rightarrow \textsf {G F} m^{tot}_{\beta }\), that is, \(\tau \models \textsf {F G} \lnot m^{tot}_{\alpha } \vee \textsf {G F} m^{tot}_{\beta }\). We divide in cases:
if \(\tau \models \textsf {F G} \lnot m^{tot}_{\alpha }\), then by the semantics of the temporal operators \(\textsf {F} \) and \(\textsf {G} \), there exists an \(i \ge 0\) such that for all \(j \ge i\), \(\tau _j \models \lnot m^{tot}_{\alpha }\). By construction of the monitors \(m^{tot}_{\alpha }\), this means that there exists an \(i \ge 0\) such that for all \(j \ge i\), \(\tau _j \models \bigvee _{k=1}^{m} \lnot m_{\alpha _k}\). This implies that, there exists a \(k \in [1,m]\) and an \(i \ge 0\) such that for all \(j \ge i\), such that \(\tau _j \models \lnot m_{\alpha _k}\). Indeed, suppose by contradiction that it is not so: then for all \(k \in [1,m]\), there exists infinitely many positions \(i \ge 0\) such that \(\tau _i \models m_{\alpha _k}\). This would mean that the monitor \(M^{tot}_{\alpha }\) is set to true infinitely many times, that is \(\textsf {G F} m^{tot}_{\alpha }\), but this is a contradiction with our hypothesis. Therefore, it holds that \(\tau \models \bigvee _{k=1}^{m} \textsf {F G} \lnot m_{\alpha _k}\), and thus also that \(\tau \models \bigwedge _{i=1}^{m} \textsf {G F} \alpha _i \rightarrow \bigwedge _{j=1}^{n} \textsf {G F} \beta _j\). Overall, since \(\tau \) is induced by \(\sigma \), we have that \(\sigma \) is a word of \(\mathcal {L}(\mathcal {A}_{ ebr })\) that induces a run \(\tau \) such that \(\tau \models \bigwedge _{i=1}^{m} \textsf {G F} \alpha _i \rightarrow \bigwedge _{j=1}^{n} \textsf {G F} \beta _j\), that is \(\sigma \in \mathcal {L}(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}})\).
If otherwise \(\tau \models \textsf {G F} m^{tot}_{\beta }\), then there exists infinitely many positions \(i \ge 0\) such that \(\tau _i \models m^{tot}_{\beta }\). Moreover, it holds that for all \(i_1 \ge 0\) and for all \(i_2 \ge i_1\), if \(\tau _{i_1} \models m^{tot}_{\beta }\) and \(\tau _{i_2} \models m^{tot}_{\beta }\), then, for all \(1 \le k \le n\), there exists a \(i_1 \le j \le i_2\) such that \(\tau _j \models m_{b_k}\). Putting together these two points, we have that for all \(1 \le k \le n\), there exists infinitely many \(i \ge 0\) such that \(\tau _i \models m_{b_k}\). That is, \(\tau \models \bigwedge _{k=1}^{n} \textsf {G F} m_{b_k}\). By definition of the monitors \(M_{\beta _i}\) and since \(\tau \) is induced by \(\sigma \), we have that \(\sigma \) is a word in \(\mathcal {L}(\mathcal {A}_{ ebr })\) that induces a run \(\tau \) such that \(\tau \models \bigwedge _{i=1}^{m} \textsf {G F} \alpha _i \rightarrow \bigwedge _{j=1}^{n} \textsf {G F} \beta _j\). That is, \(\sigma \in \mathcal {L}(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}})\).
The proof of the left-to-right direction is specular. \(\square \)
5.4 Related work
Our degeneralization step is similar to the one proposed in [37] for transforming a GR(1) condition to a one-pair Streett condition, in the context of parity game solving. The main difference is that, in this paper, we do not fix any order on the visits to the conditions \(\alpha _i\) (resp. \(\beta _i\)). For example, \(M^{tot}_{\alpha }\) is set to true whenever all the \(\alpha _i\) have been read, no matter the order. As noted in [38], this has the potential to be more effective than imposing an order to the visits (like in [37]), for example in the case where the order is \(\langle \beta _1,\beta _2,\dots ,\beta _n\rangle \) but Controller can never satisfy fairness \(\beta _{i}\) after having satisfied first the fairness \(\beta _{i+1}\).
5.5 Reduction to safety for reactivity(1) objectives
In this part, we describe a safety reduction tailored for Reactivity(1) objectives. In Sect. 6, we will prove its completeness. We will apply this reduction on the automaton \(\mathcal {A}^{\textsf {R(1)} \,}_{\textrm{degen}}\) obtained from the previous step. The intuition is to use a counter to count and limit the number of positions, after a position in which \(m^{tot}_{\beta }\) holds, in which \(m^{tot}_{\alpha } \wedge \lnot m^{tot}_{\beta }\) holds. We define the counter as follows.
Definition 18
(Counter for the reactivity(1) objective) Let \(\mathcal {A}_{\#_{\alpha ,\beta }^{\rightarrow }}^k\) be the symbolic deterministic safety automaton whose only state variable is \(\#_{\alpha ,\beta }^{\rightarrow }\), whose set of safe states is represented by the formula \(\textsf {G} (\#_{\alpha ,\beta }^{\rightarrow }< k)\) and whose transition relation is the following:
×
We define \(\mathcal {A}_{ safe }^{\textrm{k}}{:=}\mathcal {A}_{ ebr }\times \mathcal {A}_{degen} \times \mathcal {A}_{\#_{\alpha ,\beta }^{\rightarrow }}^k\), where
\(\mathcal {A}_{ ebr }\) is the product between \(\phi _{ebr}^{1}\) and \(\phi _{ebr}^{2}\) (recall Sect. 5.1);
\(\mathcal {A}_{degen}\) is the automaton obtained from \(\mathcal {A}^{\textsf {GR(1)} \,}_{\textrm{ebr}}\) (recall Sect. 5.3) by removing its accepting conditions, i.e., setting it to \(\top \); and
\(\mathcal {A}_{\#_{\alpha ,\beta }^{\rightarrow }}^k\) is the monitor defined in Def. 18.
We set the accepting condition of \(\mathcal {A}_{ safe }^{\textrm{k}}\) to be the one of \(\mathcal {A}_{\#_{\alpha ,\beta }^{\rightarrow }}^k\), i.e., \(\textsf {G} (\#_{\alpha ,\beta }^{\rightarrow }\le k)\).
The automaton \(\mathcal {A}_{ safe }^{\textrm{k}}\) is a symbolic deterministic safety automaton (recall Def. 9), and therefore it can be used as an arena for the safety game \(\langle \mathcal {A}_{ safe }^{\textrm{k}},\mathcal {C},\mathcal {U}\rangle \) (recall Def. 15). In practice, we check the realizability of \(\mathcal {A}_{ safe }^{\textrm{k}}\) by means of a tool for safety synthesis. We start with \(k=0\), and we check the realizabilty of \(\mathcal {A}_{ safe }^{\textrm{k}}\): if Controller has a strategy, we stop, otherwise we increment k and we repeat the cycle.
In the next section, we prove the soundness and the completeness of this algorithm.
6 GR-EBR synthesis: correctness via general safety reductions
In this section, we prove the (soundness and) completeness of the safety reduction described in Sect. 5. To this end, we first formalize what a safety reduction is, and then we introduce a general framework that gives sufficient conditions for obtaining complete safety reduction for arbitrary fragments of LTL . Finally, we instantiate the proposed framework to the GR-EBR case in order to prove the completeness of the algorithm of Sect. 5.
6.1 A framework of safety reductions for LTL+P realizability
The central question of this section is: how can we obtain a complete safety reduction for the realizability problem of specifications written in (fragments of)LTL ? In the following, we propose a framework to answer it.
6.2 A sound, but incomplete, safety reduction
Devising a sound and complete safety reduction for realizability is not a trivial task. Consider for example LTL . One could be tempted to define a safety reduction that, given any formula \(\phi \in \textsf {LTL} \,\), turns \(\phi \) in negated normal form (NNF, for short) and then transforms each \(\textsf {F} \) and \(\textsf {U} \) into the corresponding k-bounded operator, that is \(\textsf {F} ^{[0,k]}\) and \(\textsf {U} ^{[0,k]}\), respectively, obtaining a safety formula. The resulting reduction would be sound, since the obtained formula implies the starting one, but it would not be complete. Consider for example the formula \(\phi {:=}\textsf {G} u \leftrightarrow \textsf {G} c\). The formula obtained from \(\phi \) by means of this safety reduction is:
$$\begin{aligned} \phi _k {:=}(\textsf {F} ^{[0,k]}\lnot u \vee \textsf {G} c) \wedge (\textsf {F} ^{[0,k]}\lnot c \vee \textsf {G} u) \end{aligned}$$
Although \(\phi \) is realizable, \(\phi _k\) is unrealizable for each \(k \in \mathbb {N}\). In fact, Environment can choose u in the first k steps and \(\lnot u\) in the step \(k+1\): in this way, it falsifies both \(\textsf {F} ^{[0,k]}\lnot u\) and \(\textsf {G} u\). Since Controller can force exactly one between the formulas \(\textsf {G} c\) and \(\textsf {F} ^{[0,k]}\lnot c\), we have that \(\phi _k\) is unrealizable, and therefore this particular safety reduction is not complete for realizability.
6.3 Definition of safety reduction
The core and the main novelty of our framework is a link with safety reductions for model checking: in order to design a complete reduction for the realizability problem, one can prove that it is complete for the model checking problem and then use our framework to derive completeness for realizability. On one hand, this allows to prove completeness at the level of model checking, which is simpler than proving completeness for realizability. On the other hand, this opens the possibility of using existing safety reductions already devised for model checking for realizability as well. We start by defining what is a safety reduction in the context of our framework.
Definition 19
(Safety reduction) Let \(\mathcal {S}\subseteq \textsf {LTL} \,\) be a fragment of LTL . A safety reduction for\(\mathcal {S}\) is a function \(\llbracket \cdot \rrbracket \) such that, for each formula \(\phi \in \mathcal {S}\) over the alphabet \(\Sigma \), it holds that \(\llbracket \phi \rrbracket = \{\phi _k\}_{k \in \mathbb {N}}\), where \(\phi _k\) is a safety formula over the alphabet \(\Sigma \) such that \(\phi _k \rightarrow \phi \), for any \(k \in \mathbb {N}\). With \(\llbracket \phi \rrbracket ^{k}\), we will denote the formula \(\phi _k\) of the set \(\{\phi _k\}_{k \in \mathbb {N}}\).
6.4 Link between realizability and model checking
The rationale behind the link between realizability and model checking is the following one: since we can easily view Mealy machines as (a particular type of) Kripke structures and viceversa, and since by Prop. 2 we can restrict realizability to the search of finite strategies representable by Mealy machines, the realizability problem of the LTL+P formula \(\phi \) can be reduced to checking if there exists a Mealy machine \(M_g\) such that \(M^\prime _g \models \textsf {A} \phi \), where \(M^\prime _g\) is the Kripke structure corresponding to\(M_g\).
The Kripke structure \(M_g^\prime \)corresponding to the Mealy machine \(M_g=(2^\mathcal {U}, 2^\mathcal {C}, Q, q_0, \delta )\) is defined as \(M_g^\prime = (2^{\mathcal {U}\cup \mathcal {C}}, Q^\prime , I^\prime , T^\prime , L^\prime )\) where:
\(I^\prime = \{ (q_0, q_U, q_C) \in Q^\prime \vert \,\delta (q_0,U) = (C,q^\prime ) \text{ for } \text{ any } U \in 2^\mathcal {U}, C \in 2^\mathcal {C} \text{ and } q^\prime \in Q \}\),
3.
\(T^\prime = \{ ((q,q_U,q_C),(q^\prime , q_{U^\prime }, q_{C^\prime })) \vert \,\delta (q,U)=(C, q^\prime ) \text{ for } \text{ any } U,U^\prime \in 2^\mathcal {U}, C,C^\prime \in 2^\mathcal {C}, \text{ and } q,q^\prime \in Q^\prime \}\) and
4.
\(L^\prime ((q,q_U,q_C)) = U \cup C\).
The Kripke structure \(M_g^\prime \) is such that each trace of \(M_g^\prime \) corresponds to a word of \(M_g\), and viceversa.
In proving the completeness theorem, we will abstract from the concrete safety reduction and give the conditions for a general safety reduction \(\llbracket \cdot \rrbracket \) (as defined in Def. 19) to be complete. These conditions are formalized in Def. 20.
Definition 20
(Complete safety reduction) Let \(\mathcal {S}\subseteq \textsf {LTL} \,\) be a fragment of LTL , \(\phi \) a formula in S, and \(\llbracket \cdot \rrbracket \) a safety reduction for\(\mathcal {S}\). We say that \(\llbracket \cdot \rrbracket \) is \(\mu \)-complete, for a given function \(\mu : \mathbb {N}\rightarrow \mathbb {N}\) if and only if, for all \(\phi \in \mathcal {S}\) and for all Kripke structures M:
$$\begin{aligned} M \models \textsf {A} \phi \quad \Leftrightarrow \quad \exists k \le \mu (|M|) \cdot M \models \textsf {A} \llbracket \phi \rrbracket ^{k} \end{aligned}$$
We can finally state the main theorem of our framework, which uses Def. 20 and Prop. 2 in order to establish that if a safety reduction is complete for the model checking problem, then it is complete for the realizability problem as well.
Theorem 5
(Soundness and completeness for LTL+P realizability) Let \(\mathcal {S}\subseteq \textsf {LTL} \,\) be a fragment of LTL , \(\phi \in \mathcal {S}\) a formula over the input variables \(\mathcal {U}\) and output variables \(\mathcal {C}\) (with \(n = |\phi |\)) and \(\llbracket \cdot \rrbracket \) a \(\mu \)-complete safety reduction for \(\mathcal {S}\), for a given function \(\mu \). It holds that:
We first prove the soundness, which corresponds to the right-to-left direction. Suppose there exists a \(k \le \mu ( 2^{|\mathcal {U}|} \cdot 2^{|\mathcal {C}|} \cdot 2^{2^{c \cdot n}} )\) such that \(\llbracket \phi \rrbracket ^{k}\) is realizable. Then, there exists a strategy \(g: (2^\mathcal {U})^{+} \rightarrow 2^{\mathcal {C}}\) such that \(\mathcal {L}(g) \subseteq \mathcal {L}(\llbracket \phi \rrbracket ^{k})\). By Prop. 2, there exists a Mealy machine \(M_g = (2^\mathcal {U}, 2^\mathcal {C}, Q, q_0, \delta )\) with input alphabet \(2^\mathcal {U}\) and output alphabet \(2^{\mathcal {C}}\) such that \(\mathcal {L}(M_g) \subseteq \mathcal {L}(\llbracket \phi \rrbracket ^{k})\). Starting from \(M_g\), let \(M_g^\prime = (2^{\mathcal {U}\cup \mathcal {C}}, Q^\prime , I^\prime , T^\prime , L^\prime )\) be the corresponding Kripke structure. The Kripke structure \(M_g^\prime \) is such that each trace of \(M_g^\prime \) corresponds to a word of \(M_g\), and viceversa. Therefore all the traces \(\pi \) of \(M_g^\prime \) are such that \(L^\prime (\pi ) \models \llbracket \phi \rrbracket ^{k}\), that is \(M_g^\prime \models \textsf {A} \llbracket \phi \rrbracket ^{k}\). Since by hypothesis \(\llbracket \cdot \rrbracket \) is a \(\mu \)-complete safety reduction, by Def. 20, it holds that \(M_g^\prime \models \textsf {A} \phi \). This means that also \(\mathcal {L}(M_g) \subseteq \mathcal {L}(\phi )\). Since \(M_g\) is a Mealy machine, this implies that \(\phi \) is realizable.
We now prove completeness, which corresponds to the left-to-right direction. Suppose that \(\phi \) is realizable. Since \(\phi \in S\) and since \(S \subseteq \textsf {LTL} \,\), \(\phi \) is an LTL formula as well. Therefore, by Prop. 2, there exists a Mealy machine \(M_g\) with input alphabet \(2^\mathcal {U}\) and output alphabet \(2^\mathcal {C}\) such that \(\mathcal {L}(M_g) \subseteq \mathcal {L}(\phi )\) with at most \(2^{2^{c \cdot n}}\) states, for some constant \(c \in \mathbb {N}\). From \(M_g\), we build an equivalent Kripke structure \(M_g^\prime \) with input alphabet \(\Sigma ^\prime = 2^{\mathcal {U}\cup \mathcal {C}}\), as described above for the soundness proof. It holds that \(M_g^\prime \models \textsf {A} \phi \). Since by hypothesis \(\llbracket \cdot \rrbracket \) is a \(\mu \)-complete safety reduction for S, and since \(|Q^\prime | = 2^{|\mathcal {U}|} \cdot 2^{|\mathcal {C}|} \cdot |Q|\) (where Q and \(Q^\prime \) are the set of states of \(M_g\) and \(M_g^\prime \), respectively), by Def. 20, there exists a \(k \le \mu (2^{|\mathcal {U}|} \cdot 2^{|\mathcal {C}|} \cdot 2^{2^{c \cdot n}})\) such that \(M_g^\prime \models \textsf {A} \llbracket \phi \rrbracket ^{k}\). This means that also \(\mathcal {L}(M_g) \subseteq \mathcal {L}(\llbracket \phi \rrbracket ^{k})\). Since \(M_g\) is a Mealy machine, this means that there exists a \(k \le \mu (2^{|\mathcal {U}|} \cdot 2^{|\mathcal {C}|} \cdot 2^{2^{c \cdot n}})\) such that \(\llbracket \phi \rrbracket ^{k}\) is realizable. \(\square \)
6.5 Example
Let \(\llbracket \cdot \rrbracket _{ bo }\) and \(\llbracket \phi \rrbracket _{ bo }^{k}\) be the reduction and the formula \(\phi _k\) described in the example above, respectively (\( bo \) stands for bounded operators). Since \(\llbracket \phi \rrbracket _{ bo }^{k}\) contains only universal or bounded temporal operators, it is a safety formula; moreover, \(\llbracket \phi \rrbracket _{ bo }^{k}\) implies \(\phi \) (for any \(k\in \mathbb {N}\)); thus \(\llbracket \cdot \rrbracket _{ bo }\) is a safety reduction according to Def. 19. We have already seen that the reduction is sound but not complete for realizability. According to our framework, this reduction is not even complete for the model checking problem (i.e., with respect to Def. 20), and indeed a counterexample can be found in Fig. 1 of [11].
6.6 Novelty and usage
As already mentioned before, a distinguished and important feature of our framework is that it provides a link with safety reductions for the model checking problem. This opens the possibility to use model checking safety reductions for the realizability problem as well, provided that the reduction fulfills the requirements in Def. 20. In Sect. 6.9, we will prove that the concrete safety reduction for GR-EBR specifications that we described in Sect. 5.5 is complete with respect to Def. 20. Using Theorem 5, we will derive a corollary for the completeness of our algorithm.
6.7 In practice
The upper bound for the value of \(\mu (\cdot )\) (after which we can answer unrealizable) is doubly exponential in the size of the initial formula and therefore, in practice, it is prohibitively large. It follows that usually the completeness of a safety reduction can be exploited in practice only for making sure that, starting from a realizable specification, we will eventually find a \(k \in \mathbb {N}\) such that the \(k^{th}\) subproblem is realizable. Therefore, like K-Liveness for model checking [11], we can use our algorithm in parallel with another one that checks for the unrealizability of the specification. The first that terminates stops the other and, thus, the entire procedure.
6.8 Formalization of bounded synthesis
It is worth noting that also bounded synthesis techniques [13] can be formalized in our framework. This family of techniques works for the entire class of Universal co-Büchi Word automata (UCA , for short), which subsumes LTL+P . However, in this part, we focus only on bounded synthesis applied on LTL+P formulas. Given an LTL+P formula \(\phi \), bounded synthesis algorithms build the Büchi automaton \(\mathcal {A}_{\lnot \phi }\) for the negation of \(\phi \) (eq., the Universal co-Büchi automaton for \(\phi \)) and bound the number of times Controller player is forced to visit the set of final states of the Büchi automaton \(\mathcal {A}_{\lnot \phi }\) (eq., the set of rejecting states of the Universal co-Büchi automaton for \(\phi \)). Consider the safety automaton \(\mathcal {A}_k\) defined as \(\mathcal {A}_{\lnot \phi } \times C_k\), where \(C_k\) is the safety automaton corresponding to a counter that increments if it visits a final state of \(\mathcal {A}_{\lnot \phi }\), retains its value otherwise, and whose safe states are all those states where the counter has value less than k. We define the set of safe states of \(\mathcal {A}_k\) as the set of final states of \(C_k\). We can formalize bounded synthesis in our framework by means of a safety reduction, that we call \(\llbracket \cdot \rrbracket _{ bs }\), defined as follows: for any LTL+P formula \(\phi \) and for any \(k \in \mathbb {N}\), we define \(\llbracket \phi \rrbracket _{ bs }^{k}\) to be any safety formula (not necessarily of LTL+P ) such that \(\mathcal {L}(\llbracket \phi \rrbracket _{ bs }^{k}) = \mathcal {L}(\mathcal {A}_k)\). Note that (i) \(\llbracket \phi \rrbracket _{ bs }^{k}\) is a safety formula (since \(\mathcal {A}_k\) is a safety automaton); and (ii) \(\llbracket \phi \rrbracket _{ bs }^{k}\) implies \(\phi \) (for any \(k\in \mathbb {N}\)); thus \(\llbracket \cdot \rrbracket _{ bs }\) is a safety reduction (Def. 19). This reduction is also complete with respect to Def. 20 (see the theorem below). From now, with \(\textsf {id} : \mathbb {N}\rightarrow \mathbb {N}\) we denote the identity function.
Theorem 6
The safety reduction \(\llbracket \cdot \rrbracket _{ bs }\) is \(\textsf {id} \)-complete.
Interestingly, the proof of Theorem 6 is exactly the completeness proof of the K-Liveness algorithm by Claessen and Sörensson [11], which is a simple but very efficient algorithm for model checking based on safety reductions.
By using the main theorem of our framework (Theorem 5), we can derive the completeness of bounded synthesis for LTL+P [13, 15]. We remark that bounded synthesis works for the full class of UCA and that this is the reason why here we obtain a smaller upper bound with respect to [13, 29].
Corollary 2
(Completeness of Bounded Synthesis) Let \(\phi \) be an LTL+P formula over the set of variables \(\Sigma = \mathcal {U}\cup \mathcal {C}\). It holds that \(\phi \) is realizable if and only if there exists \(k \le 2^{|\mathcal {U}|} \cdot 2^{|\mathcal {C}|} \cdot 2^{2^{c \cdot n}}\) such that \(\llbracket \phi \rrbracket _{ bs }^{k}\) is realizable.
In this paper, we do not consider the \(\llbracket \cdot \rrbracket _{ bs }\) safety reduction, which corresponds to bounded synthesis and works with full LTL+P , because we do not know yet if there exists a fully symbolic translation from any \(\llbracket \phi \rrbracket _{ bs }^{k}\) to a safety automaton. Since one of our desiderata is to use symbolic techniques and since for \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) there exists a fully symbolic procedure for obtaining an equivalent deterministic automaton [39], we focus on fragments of LTL+P for which we can use \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) for this task. As we have seen in Sect. 5, GR-EBR is one of these.
6.9 Instantiation to GR-EBR
In this part, we prove the (soundness and) completeness of the safety reduction for GR-EBR realizability described in Sect. 5. In order to do that, we use the framework described in Sect. 6.1. We call \(\llbracket \cdot \rrbracket _{ ebr }\) the safety reduction described in Sect. 5. Since the framework works with formulas rather than with automata, for all \(\phi \in \textsf {GR} {\text{- }}\textsf {EBR} \,\), we define \(\llbracket \phi \rrbracket _{ ebr }^{k}\) to be any safety formula such that \(\mathcal {L}(\llbracket \phi \rrbracket _{ ebr }^{k}) = \mathcal {L}(\mathcal {A}_{ safe }^{\textrm{k}})\). Recall that with \(\textsf {id} : \mathbb {N}\rightarrow \mathbb {N}\) we denote the identity function.
Theorem 7
\(\llbracket \cdot \rrbracket _{ ebr }\) is a \(\textsf {id} \)-complete safety reduction for \(\textsf {GR} {\text{- }}\textsf {EBR} \,\).
Proof
We have to prove that, for all \(\phi \in \textsf {GR} {\text{- }}\textsf {EBR} \,\), for all Kripke structures M and for all \(k \in \mathbb {N}\), it holds that:
$$\begin{aligned} M \models \textsf {A} \phi \qquad \Leftrightarrow \qquad \exists k \le \textsf {id} (|M|) \cdot M \models \textsf {A} \llbracket \phi \rrbracket _{ ebr }^{k} \end{aligned}$$
We prove separately the two directions. Consider first the soundness which corresponds to the right-to-left direction. Suppose that \(M \models \textsf {A} \llbracket \phi \rrbracket _{ ebr }^{k}\). It holds that, for each initialized trace \(\pi \) of M, \(L(\pi ) \models \llbracket \phi \rrbracket _{ ebr }^{k}\), where \(L(\cdot )\) is the labeling function of M. Let \(\pi \) be an initialized trace of M. By definition of \(\llbracket \cdot \rrbracket _{ ebr }\), it holds that there exists a run \(\tau \) induced by \(L(\pi )\) such that: (i) \(\tau \) is accepting in \(\mathcal {A}_{ ebr }\times \mathcal {A}_{degen}\), and (ii) \(\tau \) is accepting in \(\mathcal {A}_{\#_{\alpha ,\beta }^{\rightarrow }}^k\). From the second point, we have that either:
\(\#_{\alpha ,\beta }^{\rightarrow }\) make infinitely many resets. This means that there exists infinitely many positions in \(\tau \) in which \(m^{tot}_{\alpha }\) holds and, after at most k occurrences of \(m^{tot}_{\alpha }\), there is a \(m^{tot}_{\beta }\). Therefore, in particular, there exists infinitely many positions in which \(m^{tot}_{\beta }\) holds, that is \(\tau \models \textsf {G F} m^{tot}_{\beta }\).
Or, the counter \(\#_{\alpha ,\beta }^{\rightarrow }\) stops to increment because, because it does not read any \(m^{tot}_{\alpha }\). This means that there exists finitely many positions in which \(m^{tot}_{\alpha }\) holds, that is \(\tau \models \textsf {F G} \lnot m^{tot}_{\alpha }\).
Therefore, it holds that \(\tau \models \textsf {F G} \lnot m^{tot}_{\alpha } \vee \textsf {G F} m^{tot}_{\beta }\), that is \(\tau \models \textsf {G F} m^{tot}_{\alpha } \rightarrow \textsf {G F} m^{tot}_{\beta }\). Finally, we have that \(\tau \) is an accepting run of \(\mathcal {A}_{ ebr }\times \mathcal {A}_{degen}\) such that \(\tau \models \textsf {G F} m^{tot}_{\alpha } \rightarrow \textsf {G F} m^{tot}_{\beta }\). Since by hypothesis \(L(\pi )\) is induced by \(\tau \), by definition of \(\mathcal {A}^{\textsf {R(1)} \,}_{\textrm{degen}}\), we have that \(L(\pi ) \in \mathcal {L}(\mathcal {A}_{ ebr }\times \mathcal {A}^{\textsf {R(1)} \,}_{\textrm{degen}})\). By concatenating Lemma 2 and Lemma 3, we have that \(L(\pi ) \in \mathcal {L}(\phi )\), and therefore \(\pi \models \phi \). It follows that \(M \models \textsf {A} \phi \).
We now prove completeness, which corresponds to the left-to-right direction. Suppose that \(M \models \textsf {A} \phi \), where \(\phi \in \textsf {GR} {\text{- }}\textsf {EBR} \,\). We prove this case by contradiction. Suppose therefore that for all \(k \le \textsf {id} (|M|)\), \(M \not \models \textsf {A} \llbracket \phi \rrbracket _{ ebr }^{k}\). This means that there exists an initialized trace \(\pi \) in M such that \(L(\pi ) \not \in \mathcal {L}(\llbracket \phi \rrbracket _{ ebr }^{k})\), for all \(k \le \textsf {id} (|M|)\). By definition of \(\llbracket \cdot \rrbracket _{ ebr }\), for \(k = \textsf {id} (|M|)\), we have that for all runs \(\tau \) induced by \(L(\pi )\) in \(\mathcal {A}_{ ebr }\times \mathcal {A}_{degen} \times \mathcal {A}_{\#_{\alpha ,\beta }^{\rightarrow }}^k\), it holds that \(\tau \not \models \textsf {G} (\#_{\alpha ,\beta }^{\rightarrow }\le k)\). Let \(\tau \) be one of these runs. There exists a position i in \(\tau \) such that \(\tau _i \models (\#_{\alpha ,\beta }^{\rightarrow }= v)\), for some \(v > k\). By definition of the counter \(\#_{\alpha ,\beta }^{\rightarrow }\), the run \(\tau \) is such that:
Recall that \(\tau \) is a run induced by \(L(\pi )\). Since \(v > k\), \(k= \textsf {id} (|M|)\) and M is a finite-state Kripke structure, the positions \(h_1 \dots h_v\) in \(\pi \) (attention: not in \(\tau \)) cannot be all different. That is, there exists at least two indexes \(s,e \in \mathbb {N}\) such that: (i) \(1 \le s < e \le v\), (ii) \(\pi _{h_s} = \pi _{h_e}\), and (iii) \(\pi _{h_s} \models m^{tot}_{\alpha }\). Starting from \(\pi \), we can build a looping trace\(\pi ^\prime \) that agrees with \(\pi \) in the prefix \(\pi _{[0,h_e]}\) and then loops on the interval \(\pi _{[h_s,h_e]}\). It holds that \(\pi ^\prime \) is an initialized trace of M and it induces a run \(\tau ^\prime \) such that \(\tau ^\prime \models \textsf {G F} m^{tot}_{\alpha } \wedge \textsf {F G} \lnot m^{tot}_{\beta }\), that is \(\tau ^\prime \not \models \textsf {G F} m^{tot}_{\alpha } \rightarrow \textsf {G F} m^{tot}_{\beta }\). Nevertheless, since \(M \models \textsf {A} \phi \), by Lemma 2 and Lemma 3, we have that \(L(\pi ^\prime ) \in \mathcal {L}(\mathcal {A}_{ ebr }\times \mathcal {A}^{\textsf {R(1)} \,}_{\textrm{degen}})\), and therefore this is a contradiction. This means that it has to hold that \(L(\pi ) \in \mathcal {L}(\llbracket \phi \rrbracket _{ ebr }^{k})\), that is \(\pi \models \llbracket \phi \rrbracket _{ ebr }^{k}\) for all the initialized traces \(\pi \) of M, and thus there exists a \(k \le \textsf {id} (|M|)\) such that \(M \models \textsf {A} \llbracket \phi \rrbracket _{ ebr }^{k}\). \(\square \)
With Theorem 5, we derive the following corollary that proves the completeness of our procedure.
Corollary 3
For any formula \(\phi \in \textsf {GR} {\text{- }}\textsf {EBR} \,\), it holds that: \(\phi \) is realizable iff \(\exists k \le \textsf {id} ( 2^{|\mathcal {U}|} \cdot 2^{|\mathcal {C}|} \cdot 2^{2^{c \cdot n}})\) such that \(\llbracket \phi \rrbracket _{ ebr }^{k}\) is realizable.
7 Related work
GR(1) has been introduced in [7, 40]. It is known that GR(1) is a good candidate for writing specifications of real-world scenarios, with a relatively low complexity: the realizability problem can be solved with at most a quadratic number of symbolic steps in the size of the specification [7]. Moreover, its importance as a specification language is accentuated by the fact that the majority of the patterns that are most commonly used in industrial specifications [41] can be compiled into GR(1) specifications [42]. Nonetheless, GR(1) presents some restrictions that limit its use as a specification language: (i) safety assumptions/guarantees are either Boolean formulas or formulas of the form \(\textsf {G} \alpha \), where the only temporal operator admitted in \(\alpha \) is the next operator \(\textsf {X} \) and no nesting of next operators is allowed; (ii) assumptions are syntactically constrained to be formulas controlled by Environment, in the sense that the variables inside the next operators of the safety part of the assumptions must be uncontrollable. In GR-EBR we relax these syntactical restrictions of GR(1) : for example, the safety assumptions and guarantees can be any arbitrary \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) formula, like, for instance, \(\textsf {G} (r \rightarrow \textsf {F} ^{[0,10]}g)\). For this reason, GR-EBR can be considered an extension not only of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) , but also of GR(1) .
On the algorithmic side, the (strict) realizability problem for GR(1) is solved in [7] by building a symbolic arena (called game structure) and by solving a fixpoint computation over it, that requires \(\mathcal {O}({N^2})\) symbolic operations, where N is the size of the specification. In this paper, we follow a different approach based on a reduction to safety, that generates a sequence of deterministic safety automata over which the corresponding game can be solved with at most a linear number of symbolic steps.
The strict semantics for the realizability problem of GR(1) is supported by many tools, including slugs [43] and spectra [44], the last one providing also advanced language features (like, for example, support for bounded counters and arithmetic operations) intended to help the writing of specifications. Interestingly, with the goal of refining the assumptions of an unrealizable GR(1) specification into a realizable one but still maintaining the assumptions as general as possible, also algorithms for computing minimal refinements of the assumptions have been proposed [45].
In [46], Morgenstern and Schneider identify a syntactical fragment of LTL , whose formulas correspond to deterministic Büchi automata. The fragment is defined in such a way that it corresponds to the temporal hierarchy defined in [27] (as a matter of fact, each formula of GR-EBR can be transformed into an equivalent one of that fragment by expanding bounded operators). Realizability is solved by exploiting known algorithms like subset construction and Miyano-Hayashi breakpoint construction for the determinization of the automata. On the contrary, the compilation of GR-EBR to automata is fully symbolic, which has been proved in [9] to be a key point for performance, compared to classical algorithms for determinization.
Bounded synthesis [13, 15] belongs to the class of Safraless techniques [14], and it consists in bounding the number of times Controller is forced to visit a rejecting state of a Universal co-Büchi automaton (UCW , for short) for the initial formula. This corresponds to a safety automaton, which can be either (i) made deterministic by a suitable generalization of the classical subset construction [29, 47], or (ii) encoded into a constraint system [13, 15] (e.g., SAT- or SMT-based) which bounds also the size of a candidate controller (this also allows one to tackle undecidable problems, for instance in the case of distributed or parametric synthesis). Both choices work for the whole class of UCW , and thus for full LTL . A significant drawback of such an approach is that the UCW , which can be exponentially larger than the initial specification, is explicitly represented. Moreover, in the first case, the algorithm for the determinization turns out to be quite complex, since each state of the resulting automaton is actually a function. This can also result into a very large state space, that can be tackled by exploiting either antichains [29] or BDDs [47]. In contrast, as we will see, we define a reduction tailored to GR-EBR formulas that allows us to exploit the \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) transformations introduced in [9] for a fully symbolic mapping of the initial formula directly into a sequence of symbolic safety automata. In particular, we never build any explicit-state automaton and we avoid the subsequent use of determinization algorithms.
Fig. 6
grace compared to BoSy (on the left) and to strix (on the right). In both plots, the two axis show the solving time (in seconds) in logarithmic scale. The red dotted lines represent the timeout (180 s)
×
ss
7.1 A short account of the tool BoSy
BoSy is a tool for reactive synthesis from LTL+P specifications based on bounded synthesis [48]. The main algorithm of BoSy takes a temporal formula \(\phi \) in input and consists of the following steps: (i) it builds the Universal co-Büchi automaton (UCW ) for \(\phi \); this automaton is built by executing one of the two tools ltl3ba [49] and spot [50], and it is explicitly represented; (ii) the automaton is optimized, e.g., by analyzing its strongly connected components [13]; (iii) the optimized automaton, along with the bound k on the visits to its rejecting states, is encoded into a constraint system (e.g., SAT, QBF, SMT) and solved by a corresponding backend. Among the different encodings, the one based on Quantified Boolean Formulas (QBF) appears to be the most efficient one in practice [15], and thus it is the default one and the one with which we compare our tool grace. Finally, BoSy starts two threads, one checking the realizability of the formula and the other checking the unrealizability. Since we will evaluate grace and BoSy only on realizable formulas (the only ones of interest in our context), in order to make fair the comparison with BoSy, we commented the part of the source code of BoSy that starts the thread for the unrealizability check.
8 Experimental evaluation
We implemented the algorithm described in Sect. 5 and summarized in Fig. 4 in a prototype tool called grace (which stands for GR-ebr reAlizability ChEcker). 2
We chose safetysynth [51] as a BDD-based backend for solving each safety game (Def. 15). safetysynth implements the classical BDD-based backward fixpoint for finding a strategy for Controller in a safety game represented in AIGER format [52].
As competitor tools, we chose BoSy [15, 48, 53] and strix [54, 55]. strix is based on parity games and is the winner of SYNTCOMP 2018, 2019 and 2020, while BoSy implements the Bounded Synthesis approach: we refer the reader to Sect. 7 for a description of Bounded Synthesis and for a description of the BoSy tool. We set a timeout of 180 seconds. The experiments have been run on a 2.7 GHz AMD 16-cores machine with 64 GB of RAM.
We remark that a comparison with GR(1) synthesis tools is nontrivial. The majority of the tools for GR(1) only support the realizability of the strict implication (see for example [43]), not the standard one (which is our case). Therefore, although the latter can be reduced to the former [7], a non-trivial practical effort is required to write an algorithm for this translation.
8.1 Description of the benchmarks set
We considered benchmarks of two types: (i) artificial, and (ii) derived from the SYNTCOMP [51] benchmarks’set. Regarding the artifical benchmarks, we partitioned them in four categories, each containing 30 benchmarks scalable in their dimension N, for a total of 120 formulas. The categories are the following ones:
The variables starting with u are uncontrollable, while those starting with c are controllable. All the benchmarks are realizable, and were specifically crafted to elicit potential criticalities of grace. The formulas in the first category consist of an implication between two \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) formulas. The second category extends the first one by adding to its assumptions (resp. the guarantees) the stabilization constraint \(\textsf {X} ^{N} \textsf {G} u_N \) (resp. \(\textsf {X} ^{N} \textsf {G} c_N \)) and a single fairness \(\textsf {G F} u_N\) (resp. \(\textsf {G F} c_N\)). In the third category, the formula corresponding to both the assumptions and the guarantees is such that half of it is safety and the other half is fairness. In particular, there are multiple fairnesses, as many as the dimension N. Finally, the benchmarks in the fourth category have been specifically designed in order to force the minimum k of the termination of grace to increase with their dimension.
Regarding the benchmarks derived from the SYNTCOMP benchmarks set, we included (i) simple_arbiter_N (for each \(N \in \{2,4,6,8,10,12\}\)), escalator_ bidirectional, which belong to the SYNTCOMP benchmarks’ set, and (ii) our example for an arbiter, with \(N \in \{1,\dots ,15\}\).
8.2 Discussion of the results
Figure 6 shows the comparison of the tools on the solving time of all the benchmarks. All times are in seconds and the scale is logarithmic. From Fig. 6 (left), we can see that almost all points are above the diagonal and, in particular, are located on the uppermost axis of the plot, which represents the timeout for the tool BoSy. This behavior involves formulas of both types (artificial and derived from SYNTCOMP), and of all four categories (of artificial benchmarks). In particular
on category 1, BoSy takes 0.5 sec. for \(N=4\) and it reaches the timeout with \(N=5\); for \(N=4\), the corresponding automaton (after optimization) has 40 states;
on category 2 (and similarly for category 3), for \(N=5\) the solving time of BoSy is 49.2 sec., and the corresponding automaton (after optimization) has 48 states; with greater values of N, BoSy reaches the timeout;
on category 4, the solving times of BoSy on \(N=13,14\) are 19.4 and 136.3 sec., respectively, and the corresponding automata have 27 and 31 states, respectively.
on simple_arbiter_N, BoSy takes 45.7 sec. for \(N=8\), and reaches the timeout for \(N=10\).
Fig. 7
Survival plot comparing the tools grace, BoSy and strix on the percentage of benchmarks solved in less than t seconds, for each \(t\in \{0,\dots ,180\}\)
Fig. 8
grace versus BoSy on number of safety sub-problems
×
×
A more precise study of the complexity of BoSy shows that the majority of the time spent by it is due to the construction of the UCW (Universal coBüchi Word automaton) corresponding to the input formula, which is the task of the tools ltl3ba and spot. On the contrary, it is clear from Fig. 6 (left) that grace avoids this bad behavior, most likely due to the fact that the explicit state UCW is never built.
Let us now consider the tool strix (Fig. 6, right). It can be noted that, on the category example-arbiter, the solving times of strix are consistently better than the ones of grace. A careful study reveals that all those benchmarks are transformed to the equi-realizable formula true by the preprocessor of Owl [56] (a tool for \(\omega \)-automata manipulation), which strix is based on.
In Fig. 7, we reported a survival plot showing, for each \(t\in \{0,\dots ,180\}\), the percentage of benchmarks solved by each of the tools in less than t seconds. An analysis of Fig. 7 shows that, although in Fig. 6 (right) there are some points below the diagonal (representing benchmarks in which strix performs better than grace), the majority of the points stands above the diagonal.
The plot in Fig. 8 shows, for each index k ranging from 1 to 31 (these correspond to the number of columns), on how many benchmarks (of both types) grace or BoSy terminate with index k (this corresponds to the height of a column). The benchmarks in category 4 and the ones of simple_arbiter_N force grace to terminate with increasing values of k. The plot in Fig. 8 points out that BoSy does not incur in this growth, except for one benchmark. Nevertheless, the solving times of grace are still better than the ones of BoSy. For example, for \(N=14\) of category 4, grace takes 20.4 sec., while BoSy takes 161 sec. This witnesses the fact that each safety sub-problem generated by grace is very simple to solve.
9 Conclusions and future work
In this paper, we proved the expressive completeness of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) with respect to the safety fragment of LTL+P . We showed also that the removal of past operators from \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) results into a loss of expressive power.
With the objective of expressing properties beyond the safety fragments while retaining an efficient synthesis problem, we introduced the logic of GR-EBR , an extension of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) [9] adding fairness conditions and assumes-guarantees formulas, and studied its realizability problem. We proposed a general framework to derive complete safety reductions in the context of realizability of (fragments of) LTL , and then we used it as the core of an algorithm for the realizability of GR-EBR formulas. The experimental evaluations showed good performance against other tools for (bounded) synthesis.
We aim at extending the work done in the following directions: (i) as far as we know, there are no safety synthesizers (like safetysynth) that are able to exploit incrementality; since in our context, the only part of the automaton that changes between one iteration and the next one is the counter, some work may be saved; (ii) stabilizing constraints are successfully used in model checking, in particular by the K-Liveness algorithm [11], in order to shrink the search of the search space; we expect that realizability may also benefit from them; (iii) since GR(1) is a very efficient fragment, it is important to investigate whether there is a compilation from GR-EBR to GR(1) ; (iv) we know that the realizability problem of GR-EBR is bounded below by EXPTIME (by EXPTIME -completeness of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) ) and bounded above by EXPTIME [2] (by EXPTIME [2]-completeness of LTL+P ): we aim at precisely characterizing its worst-case complexity; (v) last but not least, we aim at exploiting the proposed framework for more expressive logics, such as full LTL .
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, 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 licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence 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. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Obviously \(\llbracket \textsf {Normal} {\text{- }}{\textsf {LTL} _\textsf {EBR} }\,\,\rrbracket \subseteq \llbracket {\textsf {LTL} _\textsf {EBR} }\,\rrbracket \), since each formula \(\psi \) that belongs to \(\textsf {Normal} {\text{- }}{\textsf {LTL} _\textsf {EBR} }\,\,\) can be turned into an equivalent one \(\psi ^\prime \in {\textsf {LTL} _\textsf {EBR} }\,\) by expanding each bounded past operators into conjunctions/disjunctions of yesterday operators.
For proving \(\llbracket {\textsf {LTL} _\textsf {EBR} }\,\rrbracket \subseteq \llbracket \textsf {Normal} {\text{- }}{\textsf {LTL} _\textsf {EBR} }\,\,\rrbracket \), it is sufficient to apply the transformations described in [39] for the translation of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) into normal form. In particular, since by definition \(\psi \) has no past temporal operators, the only past operators in \(\psi ^\prime \) are the ones introduced by the pastification step described in [39], which are all bounded, that is either \(\textsf {Y} \) or \(\textsf {S} ^{[a,b]}\). \(\square \)
Lemma 5
Let \(d \in \mathbb {N}\). For all \(i \ge d\), for all \(j \ge i+d\), and for all \(k \ge j+d\), it holds that:
Take any value for i, j, and k such that: (i) \(i \ge d\), (ii) \(j \ge i+d\), (iii) \(k \ge j+d\). Given any interval of length d of the state sequence \({}^{i,i}\sigma ^{j}\), we show how to find an exact same one in \({}^{i,k}\sigma ^{j}\), and viceversa.
The constraints above on the three indices ensure that both the state sequences \(^{i,i}\sigma ^j\) and \(^{i,k}\sigma ^j\) contain only three types of intervals of length at most d. Consider \(^{i,k}\sigma ^j\) (the case for \(^{i,i}\sigma ^j\) is specular). The three types are the following:
Type 1:
\((\{p_1,p_2\})^n\) for some \(0 \le n \le d\);
Type 2:
\((\{p_1,p_2\})^n \cdot (\{p_1\}) \cdot (\{p_1,p_2\})^{d-n-1}\), for some \(0 \le n < d\);
Type 3:
\((\{p_1,p_2\})^n \cdot (\{p_2\}) \cdot (\{p_1,p_2\})^{d-n-1}\), for some \(0 \le n < d\);
The situation is depicted in Fig. 2. Given any interval of any of the three types above, we show below how to find the very same interval in \(^{i,i}\sigma ^j\) (Fig. 2 tries to show visually this correspondence):
each interval of \(^{i,k}\sigma ^j\) of type \((\{p_1,p_2\})^n\) is equal to \(^{i,i}\sigma ^j_{[0,n]}\);
each interval of \(^{i,k}\sigma ^j\) of type \((\{p_1,p_2\})^n \cdot (\{p_1\}) \cdot (\{p_1,p_2\})^{d-n-1}\) is equal to \(^{i,i}\sigma ^j_{[i-n,i+d-n-1]}\).
each interval of \(^{i,k}\sigma ^j\) of type \((\{p_1,p_2\})^n \cdot (\{p_2\}) \cdot (\{p_1,p_2\})^{d-n-1}\) is equal to \(^{i,i}\sigma ^j_{[j-n,j+d-n-1]}\);
This proves Property 1.
Similarly, the correspondence between intervals of \(^{i,i}\sigma ^j\) and intervals of \(^{i,k}\sigma ^j\) is the following:
each interval of \(^{i,i}\sigma ^j\) of type \((\{p_1,p_2\})^n\) is equal to \(^{i,k}\sigma ^j_{[0,n]}\);
each interval of \(^{i,i}\sigma ^j\) of type \((\{p_1,p_2\})^n \cdot (\{p_1\}) \cdot (\{p_1,p_2\})^{d-n-1}\) is equal to \(^{i,k}\sigma ^j_{[i-n,i+d-n-1]}\).
each interval of \(^{i,i}\sigma ^j\) of type \((\{p_1,p_2\})^n \cdot (\{p_2\}) \cdot (\{p_1,p_2\})^{d-n-1}\) is equal to \(^{i,k}\sigma ^j_{[j-n,j+d-n-1]}\);
This proves Property 2. \(\square \)
Lemma 6
Let \(\alpha ,\beta \in {\textsf {LTL{+}P} _\textsf {BP} }\,\), and let \(d = \max \{D(\alpha ),D(\beta )\}\) be the maximum between the temporal depths of \(\alpha \) and \(\beta \). It holds that \(\ {}^{i,i}\sigma ^j \models \alpha \textsf {R} \beta \) iff \(\ {}^{i,k}\sigma ^j \models \alpha \textsf {R} \beta \), for all \(i \ge d\), for all \(j \ge i+d\), and for all \(k \ge j+d\).
Proof
Take any value for i, j, and k such that: (i) \(i \ge d\), (ii) \(j \ge i+d\), (iii) \(k \ge j+d\). We first prove the left-to-right direction. Suppose that \({}^{i,i}\sigma ^{j} \models \alpha \textsf {R} \beta \). We divide in cases:
1.
Suppose that \({}^{i,i}\sigma ^{j}, n \models \beta \) for all \(n \ge 0\). Since \(\beta \in {\textsf {LTL{+}P} _\textsf {BP} }\,\) and \(D(\beta ) \le d\), it holds that \({}^{i,i}\sigma ^{j}_{[n-d,n]} \models \beta \), for all \(n \ge 0\). Suppose by contradiction that there exists some \(n^\prime \ge 0\) such that \({}^{i,k}\sigma ^{j}_{[n^\prime -d,n^\prime ]} \models \lnot \beta \). By Property 1 of Lemma 5, this means that there exists some \(n^{\prime \prime } \ge 0\) such that \({}^{i,i}\sigma ^{j}_{[n^{\prime \prime }-d,n^{\prime \prime }]} \models \lnot \beta \). But this is a contradiction. Thus, it holds that \({}^{i,k}\sigma ^{j}_{[n^\prime -d,n^\prime ]} \models \beta \) for all \(n^\prime \ge 0\), that is, for all \(n^\prime \ge 0\), and thus \({}^{i,k}\sigma ^{j} \models {\alpha \textsf {R} \beta }\).
2.
Suppose that \(\exists n \ge 0 \cdot ({}^{i,i}\sigma ^{j},n \models \alpha \wedge \forall 0 \le m \le n \cdot {}^{i,i}\sigma ^{j},m \models \beta )\). We divide again in cases:
(a)
Suppose that \(n<k\). Then \({}^{i,i}\sigma ^{j}_{[0,n]} = {}^{i,k}\sigma ^{j}_{[0,n]}\). Clearly, it holds that \({}^{i,k}\sigma ^{j},n \models \alpha \) and \({}^{i,k}\sigma ^{j},m \models \beta \) for all \(0 \le m \le n\). Therefore \({}^{i,k}\sigma ^{j} \models {\alpha \textsf {R} \beta }\).
(b)
Suppose that \(n \ge k\). In particular, it holds that \({}^{i,i}\sigma ^{j}_{[n-d,n]} \models \alpha \wedge \beta \). We use a contraction argument for proving that in this case there exists a smaller index at which the release satisfies its existential part (i.e., the formula \(\alpha \)). Consider the time point \(i-1\). It holds that \({}^{i,i}\sigma ^{j}_{[i-1-d,i-1]} = {}^{i,i}\sigma ^{j}_{[n-d,n]}\) and thus, since \({}^{i,i}\sigma ^{j}_{[n-d,n]} \models \alpha \wedge \beta \) and \(\alpha ,\beta \in {\textsf {LTL{+}P} _\textsf {BP} }\,\), we have that \({}^{i,i}\sigma ^{j}_{[i-1-d,i-1]} \models \alpha \wedge \beta \). Moreover, \({}^{i,i}\sigma ^{j}_{[0,i-1]}\) is a prefix of \({}^{i,i}\sigma ^{j}_{[0,n]}\), and thus, given that \({}^{i,i}\sigma ^{j}_{[p-d,p]} \models \beta \) for all \(0 \le p \le n\), it holds that \({}^{i,i}\sigma ^{j}_{[p-d,p]} \models \beta \) for all \(0 \le p \le i-1\). From this, it follows that \({}^{i,i}\sigma ^{j},i-1 \models \alpha \) and \({}^{i,i}\sigma ^{j},m \models \beta \) for all \(0 \le m \le i-1\). Since \(i-1 < k\), by Item 22a, it holds that \({}^{i,k}\sigma ^{j} \models {\alpha \textsf {R} \beta }\).
We now prove the right-to-left direction. Suppose that \({}^{i,k}\sigma ^{j} \models {\alpha \textsf {R} \beta }\). We divide in cases:
1.
Suppose that \({}^{i,k}\sigma ^{j},n \models \beta \). This case is specular to Item 1.
2.
Suppose that \(\exists n \ge 0 \cdot ({}^{i,k}\sigma ^{j},n \models \alpha \wedge \forall 0 \le m \le n \cdot {}^{i,k}\sigma ^{j},m \models \beta )\). Since \(\alpha ,\beta \in {\textsf {LTL{+}P} _\textsf {BP} }\,\) and \(D(\alpha ),D(\beta ) \le d\), it holds that \(\exists n \ge 0 \cdot ({}^{i,k}\sigma ^{j}_{[n-d,n]} \models \alpha \wedge \forall 0 \le m \le n \cdot {}^{i,k}\sigma ^{j}_{[m-d,m]} \models \beta )\). We divide again in cases:
(a)
If \(n<k\), then \({}^{i,k}\sigma ^{j}_{[0,n]} = {}^{i,i}\sigma ^{j}_{[0,n]}\) and thus \({}^{i,i}\sigma ^{j},n \models \alpha \) and \({}^{i,i}\sigma ^{j},m \models \beta \) for all \(0 \le m \le n\), that is \({}^{i,i}\sigma ^{j} \models {\alpha \textsf {R} \beta }\).
(b)
If \(k \le n \le k+d\), then \({}^{i,k}\sigma ^{j}_{[n-d,n]} = {}^{i,k}\sigma ^{j}_{[n-k-i-d,n-k-i]}\) (we used again a contraction argument). Since by hypothesis \({}^{i,k}\sigma ^{j}_{[n-d,n]} \models \alpha \), it holds also that \({}^{i,k}\sigma ^{j}_{[n-k-i-d,n-k-i]} \models \alpha \). Moreover, \({}^{i,k}\sigma ^{j}_{[0,n-k-i]}\) is a prefix of \({}^{i,k}\sigma ^{j}_{[0,n]}\), and thus, since by hypothesis \({}^{i,k}\sigma ^{j}_{[p-d,p]} \models \beta \) for all \(0 \le p \le n\), it also holds that \({}^{i,k}\sigma ^{j}_{[p-d,p]} \models \beta \) for all \(0 \le p \le n-k-i\). Therefore \({}^{i,k}\sigma ^{j}_{[n-k-i-d,n-k-i]} \models \alpha \) and \({}^{i,k}\sigma ^{j}_{[m-d,m]} \models \beta \) for all \(0 \le m \le n-k-i\). Since \(l+n-i < k\), by Item 22a, it holds that \({}^{i,i}\sigma ^{j} \models {\alpha \textsf {R} \beta }\).
(c)
Otherwise \(n > k+d\). We have that \({}^{i,k}\sigma ^{j}_{[n-d,n]} = {}^{i,k}\sigma ^{j}_{[i-1,i-1-d]}\) (also in this case we used a contraction argument). Since by hypothesis \({}^{i,k}\sigma ^{j}_{[n-d,n]} \models \alpha \), it also hold that \({}^{i,k}\sigma ^{j}_{[i-1,i-1-d]} \models \alpha \). Moreover \({}^{i,k}\sigma ^{j}_{[0,i-1]}\) is a prefix of \({}^{i,k}\sigma ^{j}_{[0,n]}\) and thus, since by hypothesis \({}^{i,k}\sigma ^{j}_{[p-d,p]} \models \beta \) for all \(0 \le p \le n\), it also holds that \({}^{i,k}\sigma ^{j}_{[p-d,p]} \models \beta \) for all \(0 \le p \le i-1\). Therefore \({}^{i,k}\sigma ^{j},i-1 \models \alpha \) and \({}^{i,k}\sigma ^{j},m \models \beta \) for all \(0 \le m \le i-1\). Since \(i-1<k\), by Item 22a, it holds that \({}^{i,i}\sigma ^{j} \models {\alpha \textsf {R} \beta }\).
\(\square \)
Lemma 7
Let \(\psi \in \textsf {Normal} {\text{- }}{\textsf {LTL} _\textsf {EBR} }\,\,\). It holds that \({}^{i,i}\sigma ^j \models \psi \) iff \({}^{i,k}\sigma ^j \models \psi \), for all \(i \ge m_\psi + d_\psi \), for all \(j \ge i+d_\psi \), and for all \(k \ge j+d_\psi \).
Proof
Take any value for i, j, and k such that: (i) \(i \ge m_\psi + d_\psi \), (ii) \(j \ge i+d_\psi \), (iii) \(k \ge j+d_\psi \). We proceed by induction on the structure of the formula \(\psi \).
For the base case, we consider three cases: (i) formulas in \({\textsf {LTL{+}P} _\textsf {BP} }\,\), that is such that all its temporal operators refer to the past and are bounded; (ii) formulas of type \(\textsf {G} \alpha \), where \(\alpha \in {\textsf {LTL{+}P} _\textsf {BP} }\,\); (iii) formulas of type \({\alpha \textsf {R} \beta }\), where \(\alpha ,\beta \in {\textsf {LTL{+}P} _\textsf {BP} }\,\);
We consider the case of a formula \(\alpha \in {\textsf {LTL{+}P} _\textsf {BP} }\,\), and suppose that \({}^{i,i}\sigma ^j \models \alpha \). By definition of \({}^{i,i}\sigma ^j\) and \({}^{i,k}\sigma ^j\), it always holds that \({}^{i,i}\sigma ^{j}_0 = {}^{i,k}\sigma ^{j}_0\). Since \(\alpha \in {\textsf {LTL{+}P} _\textsf {BP} }\,\) refers only to the current state or to the past, it follows that \({}^{i,i}\sigma ^{j} \models \alpha \) if and only if \({}^{i,k}\sigma ^{j} \models \alpha \).
Consider now the case for \({\alpha \textsf {R} \beta }\), where \(\alpha ,\beta \in {\textsf {LTL{+}P} _\textsf {BP} }\,\). Since \(m_{{\alpha \textsf {R} \beta }} = 0\) (i.e., the are no next operators in this formula), we can apply Lemma 6, having that \({}^{i,i}\sigma ^j \models {\alpha \textsf {R} \beta }\) if and only if \({}^{i,k}\sigma ^j \models {\alpha \textsf {R} \beta }\). Since \(\textsf {G} \alpha = {\bot \textsf {R} \alpha }\), this proves also the case for the globally operator.
For the inductive step, since by hypothesis \(\psi \) belongs to the normal form of \(\textsf {LTL} _\textsf {EBR} \) , it suffices to consider only the case for the next operator, conjunctions and disjunctions.
Consider first the case for the next operator, and suppose that \({}^{i,i}\sigma ^j \models \textsf {X} \psi ^\prime \). For any indices k, i and j such that \(i \ge m_{\textsf {X} \psi ^\prime }+d_{\textsf {X} \psi ^\prime }\), \(j \ge i+d_{\textsf {X} \psi ^\prime }\) and \(k \ge j+d_{\textsf {X} \psi ^\prime }\), we want to prove that \(^{i,k}\sigma ^{j} \models \textsf {X} \psi ^\prime \). By definition of the next operator, it holds that \({}^{i,i}\sigma ^j,1 \models \psi ^\prime \). Now, let \(\tau \) be the state sequence obtained from \(^{i,i}\sigma ^j\) by discarding its initial state, that is \(\tau {:=}{}^{i,i}\sigma ^j_{[1,\infty )}\). Obviously, \(\tau \models \psi ^\prime \). We observe that \(\tau \) is equal to the state sequence \(^{i-1,i-1}\sigma ^{j-1}\). Since the maximum number \(m_{\psi ^\prime }\) of nested next operators in \(\psi ^\prime \) is \(m_{\textsf {X} \psi ^\prime }-1\) (while \(\alpha _{\psi ^\prime }\) remains the same), we can apply the inductive hypothesis on \(\psi ^\prime \), having that \(^{i-1,k-1}\sigma ^{j-1} \models \psi ^\prime \).
By definition of \(\tau \), it follows that \(^{i,k}\sigma ^{j} \models \textsf {X} \psi ^\prime \).
We consider now the case for conjunctions, and suppose that \({}^{i,i}\sigma ^j \models \psi _1 \wedge \psi _2\), for generic indices k, i and j such that \(i \ge m_{\psi _1 \wedge \psi _2} + d_{\psi _1 \wedge \psi _2}\), \(j \ge i + d_{\psi _1 \wedge \psi _2}\), and \(k \ge j + d_{\psi _1 \wedge \psi _2}\).
It holds that \({}^{i,i}\sigma ^j \models \psi _1\) and \({}^{i,i}\sigma ^j \models \psi _2\). Moreover, \(m_{\psi _1} \le m_{\psi _1 \wedge \psi _2}\) and \(m_{\psi _2} \le m_{\psi _1 \wedge \psi _2}\). Similarly, \(d_{\psi _1} \le d_{\psi _1 \wedge \psi _2}\) and \(d_{\psi _2} \le d_{\psi _1 \wedge \psi _2}\). This means that we can apply the inductive hypothesis both on \(\psi _1\) and \(\psi _2\) on the current indices k, i and j. By inductive hypothesis, we have that \(^{i,k}\sigma ^j \models \psi _1\) and \(^{i,k}\sigma ^j \models \psi _2\). It follows that \(^{i,k}\sigma ^j \models \psi _1 \wedge \psi _2\). The case for \(\psi _1 \vee \psi _2\) is specular. \(\square \)
As a matter of fact, the layered structure of \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) formulas was inspired by the steps of the algorithm for the construction of symbolic automata starting from \(\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} \) -formulas. We refer the reader to [9] for details.