Regulating Synchronous Data Exchange to Meet Control Flow and Data Specifications

There are many models for formalizing multiple software components interacting with each other. E.g. in [11], smart contracts are modeled using interface automata [5]. The classic question for interface automata is to check if there exists a mediator (that can buffer method calls among the participants) such that there are no unanswered method calls [5, 10]. In [1], smart contracts are modeled in the Behavior Interaction Priority (BIP) framework, which are finite state machines (FSMs) interacting via ports. The smart contracts in [1] are part of a supply chain for crude oil, and the goal is to model check properties such as “once the point-of-sale receives the oil batches from a vendor, the payment must be triggered”. This is a typical temporal property saying one event must be followed by another.

FSMs in the BIP framework can exchange data in the form of arguments passed to method calls. We work with a model that also allows exchange of data (for example, an integer indicating the amount to be paid), but using synchronized transitions as in interface automata. In [1], control flow can be influenced by conditions such as “if the production at a vendor site is more than a specified limit, send an alert”. We model these using guards on transitions, which comprise of linear order constraints on the data exchanged. The value that is exchanged thus influences which branches can be taken by the control flow. The interoperability problem is to check if the values can be generated in such a way that the control flow remains within a specified set. The set is specified by Constraint Linear Temporal Logic (CLTL), an extension of LTL that can check linear order constraints on data values. In the above supply chain example, this can check if there exists a value for the daily production limit such that vendor and point-of-sale work together ensuring that there is always enough inventory.

We benefit from game theoretic foundations of interface automata. To tackle the interoperability problem, we design a game between two players, system and spoiler. system tries to choose values of the exchanged data (restricted to integers here) so that branches of control flow that can potentially violate the specification are disabled. spoiler tries to pick out branches in the enabled part of control flow that can potentially violate the specification. If system has a winning strategy, it provides integer values that will ensure that the specification is always met in all enabled branches of the control flow.

One difficulty that needs to be overcome is that branches in which the game can proceed depends on choices system makes from an infinite domain (integers). We handle this by designing an abstraction that reduces the game to a finite one, while still maintaining enough information about existence of winning strategies. The high level idea of using abstraction to reduce infinite domains to finite ones is a known technique [7, 3, 2, 8]. But designing the abstraction must be done carefully so that peculiarities of the original model are correctly reflected in the resulting finite symbolic model. Our first contribution is coming up with a model that is expressive enough to specify interesting properties. An example is given in Section 4. Our second contribution is designing an abstraction [definition 19] such that the resulting finite symbolic model meets two goals. First, it is equivalent to the original model wrt the existence of winning strategies [Lemma 24]. Second, it can be solved by adapting known techniques [[3], Lemma 23].

Suppose the participants do not know each other’s configurations and we need to check if they can still generate values based on the imperfect information they have. It turns out that if each participant sends integer values regularly, they can communicate their configuration information by encoding it in the integers they generate, thus communicating their configuration information to other participants and reducing it to the perfect information case. This trick will fail in other cases. It would be interesting to identify interesting fragments of the other cases where the interoperability problem makes sense.

Let $\mathbb{Z}$ be the set of integers and $\mathbb{N}$ be the set of non-negative integers. We denote by ${\lceil i\rceil }_k$ the number $i$ ceiled at $k$: ${\lceil i\rceil }_k=i$ if $i\le k$ and ${\lceil i\rceil }_k=k$ otherwise. For integers $n_1,n_2$, we denote by $[n_1,n_2]$ the set $\{n\in \mathbb{Z}\mid n_1\le n\le n_2\}$.

We recall here the definitions of constraint systems and Constraint LTL (CLTL) from [7] with some slight modifications. A constraint system $𝒟$ is of the form $(D,R_1,\mathrm{\dots },R_n,ℐ)$, where $D$ is a non-empty set called the domain. Each $R_i$ is a predicate symbol of arity $a_i$, with $ℐ(R_i)\subseteq D^{a_i}$ being its interpretation. For the sake of this paper, it suffices to describe CLTL formulas over constraint systems of the form where $D$ is an infinite domain, is a total linear order over $D$ and $=$ is the equality relation.

Let $V$ be a finite set of variables, and $A$ be a finite set of actions. A term is of the form $X^{-i}x$, where $x$ is a variable and $i\ge 0$. A constraint $c$ is of the form or $(t_i=t_j)$, where $t_i,t_j$ are terms. The syntax of CLTL is given by the following grammar, where $a\in A$ and $c$ is a constraint as defined above.

Let $F_D$ denote the set of all mappings of the form $f:V\to D$. The semantics of CLTL is defined with respect to infinite sequences over $A\times F_D$ (also called concrete models in the following).

Given a concrete model $\alpha =(a_0,f_0)(a_1,f_1)\mathrm{\dots }\in {(A\times F_D)}^{\omega }$, the $i$^th position of $\alpha$ satisfies the atomic formula $a\in A$ (written as $\alpha ,i\vDash a$) if $a=a_i$. Also, given $x,y\in V$ and $i_1,i_2\in \mathbb{N}$, the $i$^th position of a concrete model $\alpha$ satisfies the constraint (resp. $X^{-i_1}x=X^{-i_2}y$) (written as (resp. $X^{-i_1}x=X^{-i_2}y$)) if and only if $i\ge i_1,i\ge i_2$ and (resp. $f_{i-i_1}(x)=f_{i-i_2}(y)$) hold. The semantics is extended to the rest of the syntax similar to the usual propositional LTL. We use the standard abbreviations $F\varphi$ (resp. $G\varphi$) to mean that $\varphi$ is true at some position (resp. all positions) in the future. The $X$-length of a term $X^{-i}x$ is $i$. We say that a formula is of $X$-length $k$ if it uses terms of $X$-length at most $k$. The formula will be true in the first position of a concrete model if, in all positions, the value of $x$ is less than the value of $y$ in the next position and if the action $a$ holds infinitely often in the concrete model. In the rest of this paper when we refer to CLTL formulas, we shall restrict ourselves to CLTL formulas over the constraint system using just one variable $d$. The models for such formulas with just one variable can simply be thought of as sequences of the form $(a_0,v_0)(a_1,v_1)\mathrm{\dots }$ where $v_i\in \mathbb{Z}$.

We work with a model based on interface automata [5, 10]. We extend it so that integer values can be exchanged and stored.

We write $B_{𝒫},R_{𝒫},T_{𝒫}^E,T_{𝒫}^H$ to refer to the set of states, registers, external and hidden transitions of a particular FSRM $𝒫$. An $R$-valuation is a mapping from $R$ to $\mathbb{Z}$. Given an $R$-valuation $\sigma$, an integer value $v$ and a guard $g$, $\sigma ,v\vDash g$ denotes that the formula $g$ with each occurrence of $r\in R$ replaced by $\sigma (r)$ and each occurrence of $d$ replaced by $v$, evaluates to true.

In words, an external transition $t=(q,g,u,q^{\prime })$ goes from configuration $(q,\sigma )$ to $(q^{\prime },{\sigma }^{\prime })$ storing the integer value $v$ in registers belonging to $u$, provided $t$ is enabled in $\sigma$: $\sigma$ and the new integer value $v$ should satisfy the guard $g$. Hidden transitions change states without changing register valuations. We refer to the pair $(t,v)$ or $(t,\ast )$ as a step $s$.

A set of FSRMs can be composed. An output transition of one FSRM can synchronize with an input transition of another FSRM. To control which transitions can synchronize, we label them with a letter from a finite set of actions, along with one of the symbols $\{!,\mathrm{?}\}$. Transitions labeled with $!$ (resp. $\mathrm{?}$) are intended to be output (input) transitions. Two transitions can synchronize if they are labelled with the same action, one of them is additionally labeled with $!$ and the other one is additionally labeled with $\mathrm{?}$.

In the transition mentioned in point 3 above, output transition $t_o$ and input transition $t_i$ from different FSRMs synchronize by exchanging the integer value $v$. In the transition of point 4, only an output transition from an FSRM fires and we think of the environment as receiving the value, provided none of the transitions in $𝒮$ can fire to receive the value $v$. In the transition in point 5, a hidden transition in FSRM $𝒫$ fires. We refer to tuples $(a,t_o,t_i,v),(a,t_o,\ast ,v)$ and $(\ast ,t,\ast ,\ast )$ as steps.

For a step $(a,t_o,t_i,v)$ or $(a,t_o,\ast ,v)$, its projection to actions and values is ${\pi }_{av}((a,t_o,t_i,v))={\pi }_{av}((a,t_o,\ast ,v))=(a,v)$. For a step $(\ast ,t,\ast ,\ast )$ with a hidden transition $t$, ${\pi }_{av}((\ast ,t,\ast ,\ast ))=ϵ$, the empty sequence. We extend ${\pi }_{av}$ to traces as ${\pi }_{av}(c_0{s}_0{c}_1{s}_1\mathrm{\cdots })={\pi }_{av}(s_0){\pi }_{av}(s_1)\mathrm{\cdots }$. We say that a trace $\overline{\tau }$ satisfies a CLTL formula $\varphi$ (denoted as $\overline{\tau }\vDash \varphi$) if there are infinitely many external transitions fired along $\overline{\tau }$ and ${\pi }_{av}(\overline{\tau })\vDash \varphi$.

Two traces that differ only in hidden transitions can not be distinguished by CLTL formulas. We formalize this next.

A step $(a,t_o,t_i,v)$ can only be taken if the current configuration along with the new value $v$ satisfies the guards in the transitions $t_o,t_i$. Choosing certain values can thus help in avoiding traces that violate a given CLTL specification. We denote by $T_{\overline{𝒫}}^O$ the set of transitions $T_{\overline{𝒫}}^O=\{t\in T_{\overline{𝒫}}^E\mid ac(t)\in \{!\}\times A\}$.

An infinite trace $\overline{\tau }$ conforms to a regulator $\mathrm{reg}$ if the following is true: for every prefix of the form $\tau (a,t_o,t_i,v)c^{\prime }$ or $\tau (a,t_o,\ast ,v)c^{\prime }$, $v=\mathrm{reg}({[\tau ]}_{{\sim }_I},t_o)$. We say that an interface register transition system $𝒮$ is interoperable satisfying a CLTL formula $\varphi$ if there is a regulator $\mathrm{reg}$ such that all traces $\overline{\tau }$ that conform to $\mathrm{reg}$ satisfy $\varphi$.

In order to handle maximal finite traces, we add gadgets to the interface register transition system. For every action $a$, we add a sink state $s_a$. For an existing state $q$, suppose $g_1,\mathrm{\dots },g_r$ are the guards on the input transitions from $q$ labelled with $a$. We add an input transition from $q$ to $s_a$ labelled with the action $a$ and the guard $\neg (g_1\vee \mathrm{\dots }\vee g_r)$. This new transition is enabled if and only if none of the existing input transitions labelled by $a$ are enabled. On $s_a$, we have a self-loop with an output transition labelled with a new action $a^{\prime }$. On every existing state in all the FSRMs, we add self-loops with an input transition labelled with $a^{\prime }$. This way, a maximal finite play is artificially extended to an infinite one by padding ${(a^{\prime })}^{\omega }$. This can be easily identified in the CLTL specification and handled accordingly (like disallowing such actions $a^{\prime }$ as needed for the undecidability proof in appendix A).

In general, the interoperability problem for interface register transition system is undecidable. Given a 2-counter machine, we construct an interface register transition system with just two FSRMs such that the runs of the 2-counter machine are simulated by the traces of $𝒮$. It is an adaptation of similar undecidability proofs for games involving numbers, in which one player simulates a two counter machine and the other player catches mistakes if any during the simulation. For example, if the player simulating an incrementing transition increments by more than 1, it can be caught by the other player by checking that there is a value between the previous and incremented value. The details of the proof of undecidability can be found in appendix A.

In this section, we provide an example of modeling an e-commerce system with the aim of checking whether a client and a server can be made to work with each other by regulating the interaction appropriately. The example is for most parts copied from a similar example given in [10]; we add a feature to it motivating the introduction of linear order constraints in the guards of the FSRMs, which are absent in [10]. For modeling this example, we assume Interface Register Transition Systems can exchange multiple integer values in one transition. Our results can be easily extended to handle this extension.

The example models a typical online store; one FSRM for the client and one for the server. Suppose the client starts by sending a $\mathrm{𝑆𝑡𝑎𝑟𝑡𝑂𝑟𝑑𝑒𝑟}$ message containing its $\mathrm{𝑖𝑑}$ and it expects to receive an id of a new order. A schematic of the FSRM modeling the client is shown below in Figure 1.

In the figure, an edge label such as $!\mathrm{𝑆𝑡𝑎𝑟𝑡𝑂𝑟𝑑𝑒𝑟}(\mathrm{𝐶𝑙𝑖𝑒𝑛𝑡𝐼𝑑})$ means that it is a transition labeled with the action $\mathrm{𝑆𝑡𝑎𝑟𝑡𝑂𝑟𝑑𝑒𝑟}$ and the symbol $!$ (to indicate that it is a output action) and sends an integer value stored in the register named $\mathrm{𝐶𝑙𝑖𝑒𝑛𝑡𝐼𝑑}$. The client then orders a number of items via the $\mathrm{𝐴𝑑𝑑𝑇𝑜𝑂𝑟𝑑𝑒𝑟}$ action, at the end of which it provides the payment information via the $\mathrm{𝑃𝑙𝑎𝑐𝑒𝑂𝑟𝑑𝑒𝑟}$ action. Some edge labels in the figure are a quite long, so we have used shorthands such as ${\mathrm{𝑠𝑡𝑚𝑡}}_{\mathit{1}}$. These shorthands are expanded as below.

Then the client expects all items together with the quantities to be confirmed by the customer service. The client also accepts rebuttals from the customer service in case the number of items ordered is outside the minimum and maximum range allowed, via the $\mathrm{𝑂𝑢𝑡𝑂𝑓𝑅𝑎𝑛𝑔𝑒}$ message. This is a feature we have added here beyond what is described in [10], in order to demonstrate the utility of linear order constraints. The edge label $rjc{t}_i$ above implements this feature by using a guard to test that the quantity is indeed out of range. In practice, e-commerce systems would allow the client to revise the order, but for the sake of simplicity here, we just move ahead by dropping those items that are out of range. It blocks in case that it does not receive the right confirmation for the remaining items. Then it announces that it is ready to close the order and expects to receive the result of the payment transaction.

The client service expects to receive the client’s id, then it sends a confirmation and sends an id of a new order, together with a client verification. It is then prepared to repeat a loop in which it 1) receives an order of an item, 2) receives a quantity, 3) confirms the quantity or rejects as out of range and sends minimum and maximum quantity allowed. After that, it receives payment information, arranges payment via a third party service (invisible to the client and not modeled here), and sends the result of the payment transaction.

The client and customer service are not directly interoperable, since the client sends all items before accepting responses but the customer service sends responses for each item before accepting the next item. They can however still interoperate via a mediator that buffers the item orders and communicates with the two parties as expected. As done in [10], we restrict ourselves to the case where the number of items per order is bounded by a constant $n$, which becomes a parameter of the interoperability problem. The specification will say that every item is either acknowledged or out of range and that the order is closed and the result of the payment transaction is provided to the client. This can be easily specified in CLTL.

In the simulation of the two counter machine briefly mentioned at the end of Section 4 (details of which can be found in appendix A), we check that counter increments and decrements are done correctly using guards on output transitions, which ensure that the generated value is strictly between two previously generated values. It turns out that if we restrict guards on output transitions to prevent such checks, interoperability problem is decidable. Specifically, let guards on output transitions be those of the form $g:=r^i\le r^j|r^i=d|g\wedge g|\neg g$. From now on, we shall call this the restricted syntax. The new value being generated (represented symbolically by $d$ in guards) can only be tested for equality ($r_i=d$, as opposed to $r_i\le d$ in general) with register values. In other words, the restricted guards can check if the generated value is actually there in one of the registers, which is a natural test one may want to do. With guards on output transitions obeying this restricted syntax, the interoperability problem is decidable. As a first step towards proving decidability, we informally describe a game formulation of the interoperability problem.

The game is played between system and spoiler, on the transition system which is the semantics of the given interface register transition system. spoiler’s goal is to pick out a trace $\overline{\tau }$ that violates the given CLTL specification. system tries to prevent this by choosing values of the generated integers such that some transitions are disabled, thus restricting the choices available to spoiler in the next move. The game begins at the initial configuration and spoiler chooses an output transition $t_o$ labeled with some action $a$ enabled at the current configuration. system chooses a value $v$ based on the history of the play so far. spoiler chooses a transition $t_i$ enabled at some FSRM. The game moves to the updated configuration as per semantics. The game continues with the next round as before. system wins the play if the infinite trace generated by the play satisfies the CLTL specification. The existence of a winning strategy for system in this game is equivalent to the existence of a regulator.

To formally prove the above equivalence, we first formalize the game itself. A round ends with spoiler choosing an input transition that is enabled at the current configuration. The next round begins wth spoiler choosing an output transition that is enabled at the current configuration. We will combine these two moves of the spoiler and make it into a position of another game, which we call the concrete game. We denote by $T_{\overline{𝒫}}^I$ the set of transitions $T_{\overline{𝒫}}^I=\{t\in T_{\overline{𝒫}}^E\mid ac(t)\in \{\mathrm{?}\}\times A\}$.

The concrete game starts at an initial position $(c_0,t_o)$. From any position $(c_0,t_o)$, $(t_i,c,t_o)$ or $(\ast ,c,t_o)$, system makes a move by choosing a value $v\in \mathbb{Z}$. spoiler can respond by moving to any position $(t_i^{\prime },c_2,t_o^{\prime })$ (resp. $(\ast ,c_2,t_o^{\prime })$) provided the following conditions are satisfied:

• $\mathrm{■}$

  Output transition $t_o$ and input transition $t_i^{\prime }$ are labeled with the same action, say $a$ (resp. $t_o$ is labeled with $a$ and there is no input transition enabled at the configuration $c$ to receive the value $v$),

• $\mathrm{■}$

  $c{\stackrel{a,t_o,t_i^{\prime },v}{\to }}_{𝒮}{c}_1$ (resp. $c{\stackrel{a,t_o,\ast ,v}{\to }}_{𝒮}{c}_1$), $c_2$ is reachable from $c_1$ by a sequence of hidden transitions and $t_o^{\prime }$ is an output transition enabled in $c_2$.

The game then continues as before from the new position. A play is an infinite sequence of alternating positions and moves: $p_0{v}_0{p}_1{v}_1{p}_2\mathrm{\cdots }$ such that successive positions satisfy the conditions above. Histories are finite prefixes of plays, ending at positions. With every play $\pi$, we can naturally associate an infinite sequence of actions and values ${\pi }_{av}(\pi )$. system wins a play $\pi$ if ${\pi }_{av}(\pi )$ satisfies the CLTL formula $\varphi$ specified in the interoperability problem. Let $H$ denote the set of all histories.

A play $p_0{v}_0{p}_1{v}_1{p}_2\mathrm{\cdots }$ conforms to the strategy $f$ if for all $i\ge 0$, $v_i=f(p_0{v}_0\mathrm{\cdots }{p}_i)$. We say that $f$ is a winning strategy for system if all plays conforming to it are won by system.

In this section we prove that the interoperability problem for CLTL specifications is decidable when the guards on output transitions obey the restricted syntax.

We shall prove this by checking if system has a winning strategy in the associated concrete game. This is in turn checked by designing a finite parity game that is equivalent to the concrete game with respect to system having a winning strategy. We use positional determinacy of finite parity games to show this equivalence. In the rest of this section we elaborate on this.

In the concrete game, data exchanged between FSRMs come from $\mathbb{Z}$, an infinite set. We will have to simulate this in a game that can only use letters from a finite alphabet, for which we shall construct a symbolic abstraction.

We introduce the notion of partial frames and frames. We use frames (resp. partial frames) to capture the total pre-order (resp. not necessarily total pre-order) induced by the configurations and the data values along $s$ consecutive positions in the concrete game. While a partial $s$-frame captures the pre-order induced by the configurations and data values appearing in the last $s$ rounds of the concrete game upto the latest position of the spoiler, an $s$-frame extends this to a total pre-order which includes the integer value generated by system in its successive move as well.

The models of CLTL are infinite sequences over infinite alphabets. Frames, introduced in [7], abstract them to finite alphabets. Conceptually, frames and symbolic models as we will define here are almost the same as introduced in [7], where the authors used these notions to solve the satisfiability problem for CLTL. Also, in [3], the authors use the notion of frames and partial frames in CLTL games to solve the single-sided realizability problem and the notions we use here are again, quite similar.

Given an interface register transition system $𝒮=⟨\overline{𝒫},A,\mathrm{ac}⟩$ and a CLTL formula $\varphi$ over $A$ and a single variable $d$, we first define the notion of $𝒮$-variables and $𝒮$-terms.

The set of $𝒮$-variables $V_{𝒮}={\bigcup }_{𝒫\in \overline{𝒫}}{R}_{𝒫}\cup \{d\}$. An $𝒮$-term is of the form $X^{-i}x$, where $x\in V_{𝒮}$ and $i\ge 0$. For $k\ge 0$, we denote by $T_{𝒮}[k]$ the set of all $𝒮$-terms of the form $X^{-i}x$, where $i\in [0,k]$.

In the notation $s$-frame, $s$ is intended to denote the size of the frame – the number of successive positions about which information is captured. The current position and the previous $s-1$ positions are considered, for which the terms in $T_{𝒮}[s-1]$ are needed. We denote by and ${\equiv }_f$ the strict order and equivalence relation induced by iff $x{\le }_{f}y$ and $y{\nleqq }_{f}x$ and $x{\equiv }_{f}y$ iff $x{\le }_{f}y$ and $y{\le }_{f}x$.

We will deal with symbolic models that constitute sequences of frames. An $s$-frame will capture information about the first $s$ positions of a model.

An $s$-frame meant for positions $i-s$ to $i-1$ may be followed by another $s$-frame meant for positions $i-s+1$ to $i$. The two frames must be consistent about the positions $i-s+1$ to $i-1$ that they share. The following definition formalizes this requirement.

Fix a number $k\ge 0$ and consider formulas of $X$-length $k$. A symbolic model is a sequence $\rho$ of frames such that for all $i\ge 0$, $\rho (i)$ is an ${\lceil i+1\rceil }_{k+1}$-frame and $(\rho (i),\rho (i+1))$ is one-step compatible. CLTL formulas can be interpreted on symbolic models, using symbolic semantics ${\vDash }_s$ as explained next. To check if the $i$^th position of $\rho$ symbolically satisfies the atomic formula $a$, we check whether $\rho (i)$ is of the form $(a,\le )$ for some pre-order $\le$, and to check if the $i$^th position of $\rho$ symbolically satisfies the atomic constraint (where $t_1,t_2$ are terms), we check whether holds according to the total pre-order ${\le }_{\rho (i)}$ in the $i$^th frame $\rho (i)$. In formal notation, this is written as if holds. The symbolic satisfaction relation ${\vDash }_s$ is extended to all CLTL formulas of $X$-length $k$ by induction on the structure of the formula, as done for propositional LTL. To check whether in this symbolic semantics, we only need to check $\rho (i)$, the $i$^th frame in $\rho$, unlike the CLTL semantics, where we may need to check other positions also. In this sense, the symbolic semantics lets us treat CLTL formulas as if they were formulas in propositional LTL and employ techniques that have been developed for propositional LTL. But to complete that task, we need a way to go back and forth between symbolic and concrete models.

Given a concrete model $\alpha$, we associate with it a symbolic model $\mu (\alpha )$ as follows. Imagine we are looking at the concrete model through a narrow aperture that only allows us to view $k+1$ positions of the concrete model, and we can slide the aperture to view different portions. The $i$^th frame of $\mu (\alpha )$ will capture information about the portion of the concrete model visible when the right tip of the aperture is at position $i$ of the concrete model (so the left tip will be at $i-{\lceil i\rceil }_k$). Formally, the total pre-order of the $i$^th frame is the one induced by the valuations along the positions $i-{\lceil i\rceil }_k$ to $i$ of the concrete model. The action occurring in the first component of each position of the symbolic model $\mu (\alpha )$ will be the same as the action appearing in the first component of the corresponding position of the concrete model $\alpha$.

The symbolic model $\rho$ induces an order ${\le }_{\rho }$ on $\mathbb{N}\times V_{𝒮}$ as follows. Consider $i\in \mathbb{N}$ such that $\rho (i)$ contains an $s$-frame for some $s\ge 1$ and let $j\in \mathbb{N}$ be such that $j\le i$ and $i-j\le (s-1)$. We say $(i,x){⪯}_{\rho }(j,y)$ (resp. $(j,y){⪯}_{\rho }(i,x)$) if $x{\le }_{\rho (i)}{X}^{j-i}y$ (resp. $X^{j-i}y{\le }_{\rho (i)}x$). In other words, for the variables and positions captured in the frame $\rho (i)$, ${⪯}_{\rho }$ is same as the total pre-order ${\le }_{\rho (i)}$ over that frame. Now we define ${\le }_{\rho }$ to be the transitive closure of ${⪯}_{\rho }$ and to be the transitive closure of ${\prec }_{\rho }$. ${\le }_{\rho }$ is now a partial order over $\mathbb{N}\times V_{𝒮}$.

For every concrete model, there is an associated symbolic model, but the converse is not true. We say that a symbolic model $\rho$ admits a concrete model if there exists a concrete model $\alpha$ such that $\rho =\mu (\alpha )$. In particular, it is easy to see that if there are infinite chains of the form that we shall define below in a symbolic model then it does not admit a concrete model.

If a symbolic model $\rho$ has an infinite chain as above, the integer values associated with $(i_2,x),(i_3,x)\mathrm{\dots }$ will all be distinct from each other and will be inside the interval from $(i_1,x)$ to $(j_1,y)$, which is impossible. Hence, absence of infinite chains is a necessary condition for a symbolic model to admit concrete models. We shall see later that this is also a sufficient condition for a subset of symbolic models

We next define partial frames and compatibility between a partial frame and a frame.

Figure 2 illustrates $s$-frames, partial $s$-frames and one-step compatibility graphically. Observe here that the pairs $(f_1,p{f}_2)$ and $(p{f}_2,f_2)$ are both one-step compatible. Note that the figure does not indicate some of the edges in the 3-frame and partial 3-frame which can be inferred using transitivity.

We now begin defining the symbolic game. We first define the notion of a symbolic configuration. A pair $(\overline{q_P},f)$ where $f$ is any ${\lceil s\rceil }_{k+1}$-frame for some $s\ge 1$, is called a symbolic configuration (denoted by $sc$). We call $(\overline{q_P},\mathrm{𝑝𝑓})$ a partial symbolic configuration (denoted by $psc$) where $\mathrm{𝑝𝑓}$ is any partial ${\lceil s\rceil }_{k+1}$ -frame for some $s\ge 1$. Given a transition $t=(q,g,u,q^{\prime })$, a tuple of states $\overline{q_P}$ and a ${\lceil s\rceil }_{k+1}$-frame $f$, we say $t$ is enabled at $(\overline{q_P},f)$ if the action label of $t$ is same as the first component of $f$, $q\in \overline{q_P}$ and the frame $f$ satisfies the guard $g$, or in other words, $r_{𝒫}^i{\le }_f{r}_{𝒫}^j$ holds if $g=r_{𝒫}^i\le r_{𝒫}^j$ and $r_{𝒫}^i{\le }_{f}d$ holds if $g=r_{𝒫}^i\le d$. We next define the notions of symbolic updates and symbolic steps which we shall use to design the rules of the finite parity game simulating the concrete game.

We know that any LTL formula $\varphi$ can be converted to an equivalent non-deterministic Büchi automaton with an exponential number of states in the size of $\varphi$ in EXPTIME [15]. Now, every non-deterministic Büchi automaton with $n$ states can be converted to a deterministic parity automaton [9, Chapter 1] with number of states exponential in $n$ and number of colours polynomial in $n$ [13, Theorem 3.10]. Using these results, it is easy to see that given a CLTL formula $\varphi$, we can construct a deterministic parity automaton ${𝒜}_{\varphi }$ with set of states $Q$ and with number of colours $l$, accepting the set of all sequences of frames that symbolically satisfy $\varphi$, such that $|Q|$ is double exponential in the size of $\varphi$ and $l$ is exponential in the size of $\varphi$.

In order to construct a winning strategy for system in the concrete game using a winning strategy for system in the symbolic parity game that we shall construct, we also need to ensure that every sequence of frames resulting from a play of the game conforming to the winning strategy admits integer labellings for every variable in each of the frames. As done in [7] and [3], it is possible to construct a Büchi automaton of size polynomial in the size of the formula $\varphi$ and hence a deterministic parity automaton ${𝒜}_{chain}$ of size exponential in the size of $\varphi$ that checks for the absence of infinite chains in a symbolic model $\rho$ satisfying $\varphi$. We shall use ${𝒜}_{\varphi }$ and ${𝒜}_{chain}$ to define the parity winning condition of the symbolic game and we will see later that this ensures the existence of winning strategies with integer labellings for the sequence of frames along every play conforming to certain type of winning strategies.

We denote the set of spoiler positions by $P_{spo}$ and set of system positions by $P_{sys}$ The symbolic game starts at an initial position $(\overline{q_{𝒫}^0},{\mathrm{𝑝𝑓}}_0,t_o,q_I)$. From any position $(\overline{q_{𝒫}^0},{\mathrm{𝑝𝑓}}_0,t_o,q_I)$, $(t_i,\overline{q_{𝒫}},\mathrm{𝑝𝑓},t_o,q)$ or $(\ast ,\overline{q_{𝒫}},\mathrm{𝑝𝑓},t_o,q)$, system makes a move by choosing a position $(\overline{q_{𝒫}^0},f_0,t_o,q_I)$, $(t_i,\overline{q_{𝒫}},f,t_o,q)$ or $(\ast ,\overline{q_{𝒫}},f,t_o,q)$ where $f_0$ is the $1$-frame with all register variables and the variable $d$ equal to each other and $f$ is a frame such that $(pf,f)$ is one-step compatible and is such that $f$ satisfies the guard $g$ appearing in $t_o$.

spoiler can respond by moving to any position $(t_i^{\prime },{\overline{q_{𝒫}}}^{\prime },{\mathrm{𝑝𝑓}}^{\prime },t_o^{\prime },q^{\prime })$ (resp. $(\ast ,{\overline{q_{𝒫}}}^{\prime },{\mathrm{𝑝𝑓}}^{\prime },t_o^{\prime },q^{\prime })$) provided the following conditions are satisfied:

• $\mathrm{■}$

  There is a symbolic step from $(\overline{q_{𝒫}},f)$ to $({\overline{q_{𝒫}}}^{\prime \prime },{\mathrm{𝑝𝑓}}^{\prime })$ on $(a,t_o,t_i^{\prime })$ or $(\ast ,t_o,t_i^{\prime })$ as defined in 18 and ${\overline{q_{𝒫}}}^{\prime }$ is reachable from ${\overline{q_{𝒫}}}^{\prime \prime }$ by a sequence of hidden transitions. Formally, $(\overline{q_{𝒫}},f){\stackrel{(a,t_o,t_i^{\prime })}{\to }}_{𝒮}({\overline{q_{𝒫}}}^{\prime \prime },{\mathrm{𝑝𝑓}}^{\prime })$ (resp. $(\overline{q_{𝒫}},f){\stackrel{(a,t_o,\ast )}{\to }}_{𝒮}({\overline{q_{𝒫}}}^{\prime \prime },{\mathrm{𝑝𝑓}}^{\prime })$).

• $\mathrm{■}$

  Transition $t_o^{\prime }$ is enabled at the partial symbolic configuration $({\overline{q_{𝒫}}}^{\prime },{\mathrm{𝑝𝑓}}^{\prime })$

• $\mathrm{■}$

  There is a transition from $q$ to $q^{\prime }$ on reading the frame $f$ in the deterministic parity automaton $𝒜$.

The game then continues as before from the new position. A play is an infinite sequence of alternating spoiler and system positions: $p_0{p}_0^{\prime }{p}_1{p}_1^{\prime }{p}_2{p}_2^{\prime }\mathrm{\cdots }$ such that successive positions satisfy the conditions above. Histories are finite prefixes of plays, ending at spoiler positions. system wins a play of the game if the parity condition is satisfied by the play. Let $H$ denote the set of all histories. Given a play $\pi$, let ${\pi }_f(\pi )$ be the projection of the play to the underlying sequence of frames contained in each system position.

A play $p_0{p}_0^{\prime }{p}_1{p}_1^{\prime }{p}_2{p}_2^{\prime }\mathrm{\cdots }$ conforms to the strategy (resp. positional strategy) $st$ if for all $i\ge 0$, $p_i^{\prime }=st(p_0{v}_0\mathrm{\cdots }{p}_i)$ (resp. $p_i^{\prime }=st(p_i)$). We say that a strategy/positional strategy $st$ is a winning strategy for system if all plays conforming to it are won by system. We abuse notation and say $t_1{\le }_{p^{\prime }}{t}_2$ for $t_1,t_2\in V_{𝒮}$ and $p^{\prime }\in P_{sys}$ to mean $t_1{\le }_f{t}_2$ where $f$ is the frame contained in position $p^{\prime }$.

We associate a finitely branching infinite tree with a positional strategy $st$. Let ${\mathrm{\Pi }}_{st}$ be the collection of all plays that conform to strategy $st$ and let $H_{st}$ be the collection of all finite prefixes of plays in ${\mathrm{\Pi }}_{st}$ ending in a spoiler position. Now let ${\pi }_{spo}(H_{st})$ denote the projection of such histories to just the sequence of spoiler positions. Now we define a tree associated with positional strategy $st$ as $T:{\pi }_{spo}(H_{st})\to P_{sys}$ given by $T(p_0{p}_1\mathrm{\dots }{p}_i)=st(p_i)$. For every node $\eta$ in $T$, its set of children corresponds to the set of spoiler moves possible for the system move $T(\eta )$. For a node $\eta$, the subtree $T_{\eta }$ rooted at $\eta$ is such that for all ${\eta }^{\prime }$, $T_{\eta }({\eta }^{\prime })=T(\eta \cdot {\eta }^{\prime })$. A tree $T$ is called regular if the set $\{T_{\eta }\mid \eta \in {\pi }_{spo}(H_{st})\}$ is finite, i.e., there are only finitely many subtrees up to isomorphism. Two nodes $\eta ,{\eta }^{\prime }$ are said to be isomorphic if $T_{\eta }=T_{{\eta }^{\prime }}$. It is easy to verify that the tree $T$ associated with a positional winning strategy is a regular tree.

Given an infinite path $\pi \in {\pi }_{spo}({\mathrm{\Pi }}_{st})$ of the tree $T$, we associate with it, a symbolic model $\rho$, which is the infinite sequence of frames obtained from the labels of the nodes along that path.

We now give an automata-theoretic characterization for trees that are labellable. Using the fact that the trees associated with positional strategies are regular and using results from [3], we get that such trees are labellable if and only if the symbolic model associated with each infinite path of the tree does not have any infinite chain. Recall that the automaton ${𝒜}_{chain}$ we defined earlier, checks for absence of infinite chains in a symbolic model and therefore, we get the following lemma:

Now, we know that if a positional strategy is winning, then the sequence of frames along every play conforming to the strategy must not have any infinite chains, hence no path in the tree associated with this strategy should have any infinite chains. Using Lemma 22, we then get that:

We now extend the map $\mu$ to go from histories $h_c$ (resp. plays ${\pi }_c$) of the concrete game to histories $h_s$ (resp. plays ${\pi }_s$) of the symbolic game. We define a function $\mu :H_c\to H_s$ as follows: $\mu ((c_0,t_0)v_0(t_0^{\prime },c_1,t_1)v_1\mathrm{\dots }(t_i^{\prime },c_{i+1},t_{i+1}))$ equals $(\overline{q_{𝒫}^0},{\mathrm{𝑝𝑓}}_0,t_0,q_I)(\overline{q_{𝒫}^0},f_0,t_0,q_I)(t_0^{\prime },\overline{q_{𝒫}^1},{\mathrm{𝑝𝑓}}_1,t_1,q_1)(t_0^{\prime },\overline{q_{𝒫}^1},f_1,t_1,q_1)\mathrm{\dots }(t_i^{\prime },\overline{q_{𝒫}^{i+1}},{\mathrm{𝑝𝑓}}_{i+1},t_{i+1},q_{i+1})$ where ${\mathrm{𝑝𝑓}}_j$ is the partial ${\lceil j+1\rceil }_{k+1}$-frame induced by the configurations $c_{j-{\lceil j\rceil }_{k+1}},\mathrm{\dots }{c}_j$ and the integer values $v_{j-{\lceil j\rceil }_{k+1}},\mathrm{\dots }{v}_{j-1}$ and $f_j$ is the ${\lceil j+1\rceil }_{k+1}$-frame induced by the configurations $c_{j-{\lceil j\rceil }_{k+1}},\mathrm{\dots }{c}_i$ and the integer values $v_{j-{\lceil j\rceil }_{k+1}},\mathrm{\dots }{v}_j$, $\overline{q_{𝒫}^j}$ is the tuple of states in configuration $c_j$ and $q_j$ is the state of DPA $𝒜$ on reading the sequence of frames $f_0\mathrm{\dots }{f}_{j-1}$ for all $0\le j\le i$. $\mu$ is defined over plays of the concrete game in a similar manner. We now use all the above definitions and lemmas to establish the equivalence between the concrete and the symbolic games.