Synthesizing Skeletons for Reactive Systems

TL;DR

This paper introduces a novel analysis technique called skeletons for reactive systems, which visualizes which parts of a system's implementation are determined or still open based on temporal specifications, aiding in verification and synthesis.

Contribution

It presents algorithms for verifying and learning skeletons from LTL specifications, enabling better understanding and repair of underspecified reactive system requirements.

Findings

Skeletons represent output possibilities with three-valued logic.

Algorithms efficiently verify and synthesize skeletons from LTL specifications.

Technique helps identify and fix underspecified critical system behaviors.

Abstract

We present an analysis technique for temporal specifications of reactive systems that identifies, on the level of individual system outputs over time, which parts of the implementation are determined by the specification, and which parts are still open. This information is represented in the form of a labeled transition system, which we call skeleton. Each state of the skeleton is labeled with a three-valued assignment to the output variables: each output can be true, false, or open, where true or false means that the value must be true or false, respectively, and open means that either value is still possible. We present algorithms for the verification of skeletons and for the learning-based synthesis of skeletons from specifications in linear-time temporal logic (LTL). The algorithm returns a skeleton that satisfies the given LTL specification in time polynomial in the size of the minimal skeleton. Our new analysis technique can be used to recognize and repair specifications that underspecify critical situations. The technique thus complements existing methods for the recognition and repair of overspecifications via the identification of unrealizable cores.

Full text

1 Introduction

The great advantage of synthesis is that it constructs an implementation automatically from a specification – no programming required. The great disadvantage of synthesis is that the synthesized implementation is only as good as its specification, and writing good specifications is extremely difficult.

Roughly speaking, there are two fundamental errors that can happen when writing a specification. The first type of error is to overspecify the system such that actually no implementation exists anymore. This type of error can be found by a synthesis algorithm (it fails!), and synthesis tools commonly assist in the repair of such errors by identifying an unrealizable core of the specification (cf. [1, 11, 12]). The second type of error is to underspecify the system such that not all implementations that satisfy the specification actually perform as intended. This type of error is much harder to detect. The synthesis succeeds, and even if we convince ourselves that the synthesis tool has actually chosen an implementation that performs as intended, there is no guarantee that this will again be the case when a new implementation is synthesized from the same or an extended specification.

The underlying problem is that synthesis algorithms have the freedom to resolve any underspecified behavior in the specification, and we have no way of knowing which parts of the behavior were fixed by the specification, and which parts were chosen by the synthesis algorithm.

In this paper, we introduce a new artifact that can be produced by synthesis algorithms and which provides exactly this information. We call this artifact the skeleton of the specification. We envision that synthesis algorithms would produce the skeleton along with the actual implementation, so that the user of the algorithm understands where the implementation is underspecified, and can, if so desired, strengthen the specification in critical areas.

A skeleton is a labeled transition system defined over three-valued sets of atomic propositions, where in each state of the skeleton an atomic proposition is either true, false, or open. For a given specification, the truth value of a proposition in some state of the skeleton is open if it can be replaced by $\mathit{true}$ as well as by $\mathit{false}$ without violating the specification. Consider for example the LTL formula $\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}p$ for some atomic proposition $p$. Any transition system that satisfies the formula has truth value $\mathit{true}$ for $p$ in the second position of every path of the transition system. On the other hand, whether $p$ is $\mathit{true}$ or $\mathit{false}$ in the initial state is not determined, either truth value would work. In this case, the skeleton would not fix a particular truth value, but rather leave the value of $p$ in the initial state open. In a sense, the skeleton implements only those parts of the transition system that are determined by the specification.

Skeletons are useful to understand the meaning of partially written specifications. Consider, for example, an arbiter over two clients that share some resource. Each client can make a request to the source (via the inputs $r_{1}$ and $r_{2}$) and the arbiter can, accordingly, decide to give out grants via the outputs $g_{1}$ and $g_{2}$. A specification for the arbiter might begin with the property of mutual exclusion, i.e., the LTL formula $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(\bar{g}_{1}\vee\bar{g}_{2})$ stating that only one of the clients should have access to the resource at a time. Figure 1 shows an implementation of this specification as a transition system and a skeleton. The transition system has a single state, and no grants are given at any time (see Figure 1). The skeleton shown in Figure 1 reveals that all outputs are open, as indicated by the question mark. If we extend the specification with the property $\bar{g}_{1}\wedge\bar{g}_{2}$, then the previous transition system does not need to change, because it already satsifies the extended specification. The skeleton, on the other hand, now indicates that the output in the initial state is determined. The output in subsequent states is still open (see Figure 1(a)). Extending the specification further with the property $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(r_{1}\rightarrow\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}g_{1})$ results in a skeleton where the responses to requests from the first client are determined, and outputs in situations where there is no request from the first client are still open (see Figure 1). An implementation for this specification could be the transition system that never gives a grant to the second client (see Figure 1).

We study the model checking and synthesis problems for skeletons. For a given LTL formula $\varphi$ and a skeleton $\mathcal{S}$ we say that $\mathcal{S}$ is a model of the LTL formula $\varphi$, if each trace in $\mathcal{S}$ satisfies following condition: If the truth value for some proposition $p$ in some position of the trace is open, then $\varphi$ must both have a model where $p$ is $\mathit{true}$ at this position, and a model where $p$ is $\mathit{false}$ at this position. Furthermore, if the trace has truth value true or false for $p$ at some position, then all models of $\varphi$ map $p$ to the truth value true or false, respectively, at this position.

We show that given an LTL formula $\varphi$ we can build a nondeterministic automaton that accepts a sequence over the three-valued semantics if it satisfies the satisfaction relation described above. The automaton is of doubly-exponential size in the length of the formula $\varphi$. With this automaton, the model checking problem can be solved in Expspace.

To solve the synthesis problem, we could determinize the automaton and check whether there is a skeleton for the formula, along the lines of standard synthesis [16], but this construction would be very expensive. Instead, we introduce a synthesis algorithm for skeletons based on learning. We show that for each LTL formula, a skeleton that models the formula defines a safety language that can be learned using the learning algorithm L∗. The algorithm can learn a skeleton for an LTL formula in time polynomial in the size of the minimal skeleton for the specification. The membership and equivalence queries of the L∗ algorithm are answered by the model checking algorithm introduced in this paper.

Related Work.

There is a rich body of work on the synthesis of reactive systems from logical specifications [7, 4, 10, 13, 14]. Supplemented by many works that investigated the optimization of specification for synthesis and the identification of unrealizable specification [11, 12, 1]. Multi-valued extensions of logics have been rather popular in the verification of systems, where a simple truth value is not enough to determine the quality of implementations. Chechik et. al. provide a theoretical basis for multi-valued model checking [6], where the satisfaction relation $\mathcal{M}\models\varphi$ for a model $\mathcal{M}$ and a specification $\varphi$ can be multi-valued. Bruns and Godefroid experiment on multi-valued logics and show that many algorithms for multi-valued logics can be reduced to ones for two-valued logics [5]. Easterbrook and Chechik introduce a framework where multiple inconsistent models are merged according to an underlying specification given in a multi-valued logic, where the different values in the specification represent the different levels of uncertainty, priority and agreement between the merged models [9]. In comparison to all these works, we are interested in multi-valued extensions of the models themselves and in the synthesis of such models, in order to determine the amount of information that resides in a specification.

The term skeleton has been also used by Emerson and Clarke which shall not be confused with the skeletons presented here. They presented a method for the synthesis of synchronization skeletons that abstract from details irrelevant to synchronization of concurrent systems [8]. In our skeletons, we stick to the structure of transition systems and leave place holders for the underspecified details, which may then be supplemented with further steps to a complete transition system.

2 Preliminaries

Alternating Automata.

We define an alternating Büchi automaton as a tuple $\mathcal{A}=(\Sigma,Q,q_{0},\delta,F)$, where $\Sigma$ denotes a finite alphabet, $Q$ denotes a finite set of states, $q_{0}\in Q$ denotes a designated initial state, $\delta:Q\times\Sigma\rightarrow\mathbb{B}^{+}(Q)$ denotes a transition function, that maps a state and an input letter to a positive boolean combination of states, and finally the set $F\subseteq Q$ of accepting states.

We define infinite words over $\Sigma$ as sequence $\sigma:\mathbb{N}\rightarrow\Sigma$. A $\Sigma$-tree is a pair $(\mathcal{T},r)$ over a set of directions $D$, where $\mathcal{T}$ is a prefix-closed subset of $D^{*}$ and $r:\mathcal{T}\rightarrow\Sigma$ is a labeling function. The empty sequence $\epsilon$ is called the root. The children of a node $n\in\mathcal{T}$ are nodes $C(n)=\{n\cdot d\in\mathcal{T}\mid d\in D\}$.

A run of an automaton $\mathcal{A}=(\Sigma,Q,q_{0},\delta,F)$ on a sequence $\sigma:\mathbb{N}\rightarrow\Sigma$ is a $Q$-tree $(\mathcal{T},r)$ with $r(\epsilon)=q_{0}$ and for all nodes $n\in\mathcal{T}$, if $r(n)=q$ then the set $\{r(n^{\prime})\mid n^{\prime}\in C(n)\}$ satisfies $\delta(q,\sigma(|n|))$.

A run $(\mathcal{T},r)$ is accepting if for every infinite branch $n_{0},n_{1},\dots$ the sequence $r(n_{0})r(n_{1})\ldots$ satisfies the Büchi condition, which requires that some state from $F$ occures infinitely often in the sequence $r(n_{0})r(n_{1})\ldots$.

The set of accepted words by the automaton $\mathcal{A}$ is the language of the automaton and is denoted by $L(\mathcal{A})$. An automaton is empty iff its language is the empty set.

A nondeterministic automaton is a special alternating automaton, where the image of $\delta$ consists only of such formulas that, when rewritten in disjunctive normal form, contain exactly one element of $Q$ in every disjunct.

An alternating automaton is called universal if, for all states $q$ and input letters $\alpha$, $\delta(q,\alpha)$ is a conjunction. A universal and nondeterministic automaton is called deterministic.

A Büchi automaton is called a safety automaton if $Q=F$. Safety automata are denoted by a tuple $(\Sigma,Q,q_{0},\delta)$. For safety automata, every run graph is accepting.

The dual of Büchi automata are co-Büchi automata. In a co-Büchi automaton the set $F$ is a set of rejecting states and a run is accepting if it has only finitely many appearances of states in $F$.

Safety Languages:

A finite word $w=\{1,\dots,i\}\rightarrow\Sigma$ over some finite alphabet $\Sigma$ is called a bad-prefix for a language $L\subseteq\Sigma^{\omega}$, if every infinite word $\sigma\in(\mathbb{N}\rightarrow\Sigma)$ with prefix $w$ is not in the language $L$. A language $L\subseteq(\mathbb{N}\rightarrow\Sigma)$ is called a safety language, if every $\sigma\not\in L$ has a bad-prefix. We denote the set of bad-prefixes for a language $L$ by $\emph{BP}(L)$. For every safety language $L$ we can define a finite word automaton $\mathcal{B}=(Q_{\mathcal{B}},Q_{\mathcal{B},0},F_{\mathcal{B}},\delta_{\mathcal{B}})$ that accepts the language $\emph{BP}(L)$. We call $\mathcal{B}$ the bad-prefix automaton of $L$.

Linear-time Temporal Logic:

We use Linear-time Temporal Logic (LTL) [15], with the usual temporal operators Next $\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$, Until $\cal U$ and the derived operators Eventually $\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ and Globally $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$. LTL formulas are defined over a set of atomic propositions $\textit{AP}=I\cup O$, which is partitioned into a set $I$ of input propositions and a set $O$ of output propositions. We denote the satisfaction of an LTL formula $\varphi$ by an infinite sequence $\sigma\colon\mathbb{N}\rightarrow 2^{\textit{AP}}$ of valuations of the atomic propositions by $\sigma\models\varphi$. For an LTL formula $\varphi$ we define the language $L(\varphi)$ by the set $\{\sigma\in(\mathbb{N}\rightarrow 2^{\textit{AP}})\mid\sigma\models\varphi\}$.

Implementations:

We represent implementations as labeled transition systems. For a given finite set $\Upsilon$ of directions and a finite set $\Sigma$ of labels, a $\Sigma$-labeled $\Upsilon$-transition system is a tuple $\mathcal{T}=(T,t_{0},\tau,o)$, consisting of a finite set of states $T$, an initial state $t_{0}\in T$, a transition function $\tau\colon T\times\Upsilon\rightarrow T$, and a labeling function $o\colon T\rightarrow\Sigma$. A path in $\mathcal{T}$ is a sequence $\pi\colon\mathbb{N}\rightarrow T\times\Upsilon$ of states and directions that follows the transition function, i.e., for all $i\in\mathbb{N}$ if $\pi(i)=(t_{i},e_{i})$ and $\pi(i+1)=(t_{i+1},e_{i+1})$, then $t_{i+1}=\tau(t_{i},e_{i})$. We call a path initial if it starts with the initial state: $\pi(0)=(t_{0},e)$ for some $e\in\Upsilon$. We denote the set of initial paths of $\mathcal{T}$ by $\emph{Path}(T)$. For a path $\pi\in\emph{Path}(T)$, we denote the sequence $\sigma_{\pi}\colon i\mapsto o(\pi(i))$, where $o(t,e)=(o(t)\cup e)$ by the trace of $\pi$. We call the set of traces of the paths of a transition system $\mathcal{T}$ the language of the $\mathcal{T}$, denoted by $L(\mathcal{T})$.

For a set of atomic propositions $\textit{AP}=O\cup I$, we say that a $2^{O}$-labeled $2^{I}$-transition system $\mathcal{T}$ satisfies an LTL formula $\varphi$, if and only if $L(T)\subseteq L(\varphi)$, i.e., every trace of $\mathcal{T}$ satisfies $\varphi$. In this case we call $\mathcal{T}$ a model of $\varphi$.

Multi-valued Sets:

A multi-valued set over an alphabet $\Sigma$ and set of values $\Gamma$ is a function $v\in(\Sigma\rightarrow\Gamma)$. The simplest type of multi-valued sets is the two-valued set which define the notion of sets as we know, where $\Sigma$ is a set of symbols and $\Gamma=\{\bot,\top\}$, i.e., for a two-valued set $v$ over $\Sigma$ and $\Gamma$, a symbol $a\in\Sigma$ is in $v$ if $v(a)=\top$, and not otherwise. The set of all multi-valued sets over an alphabet $\Sigma$ and a set of values $\Gamma$ is denoted by $\Gamma^{\Sigma}$, e.g., in the usual set notion this is the set $\{\bot,\top\}^{\Sigma}$ or as we know it $2^{\Sigma}$ for an alphabet $\Sigma$.

For a multi-valued set $v\in\Gamma^{\Sigma}$ and for $p\in\Sigma$ and $h\in\Gamma$ we define the multi-valued set $v^{\prime}=v[p\mapsto h]$, where $v^{\prime}(p)=h$ and for all $p^{\prime}\in\Sigma\setminus\{p\}$, we have $v^{\prime}(p^{\prime})=v(p^{\prime})$. For a multi-valued set $v\in\Gamma^{\Sigma}$ and for a set $\Sigma^{\prime}\subseteq\Sigma$ the set $v_{\Sigma^{\prime}}\in\Gamma^{\Sigma^{\prime}}$ is the multi-valued set obtained by projection from $\Sigma$ to $\Sigma^{\prime}$.

3 Skeletons

An open set over an alphabet $\Sigma$ is a three-valued set $v:\{\top,\bot,?\}^{\Sigma}$, where each element $a\in\Sigma$ is either in $v$ denoted by $v(a)=\top$, not in $v$ denoted by $v(a)=\bot$, or it is open whether it is in the set or not, i.e., it could be one of both, denoted by $v(a)=?$. In the remainder of the paper, we denote the set $\{\top,\bot,?\}^{\Sigma}$ by $3^{\Sigma}$. For two open sets $v,v^{\prime}\in 3^{\Sigma}$ we define the partial order $\sqsubseteq$ such that $v\sqsubseteq v^{\prime}$ if and only if for all symbols $a\in\Sigma$, $v(a)\preceq v^{\prime}(a)$ with respect to the lattice $\preceq=\{(\bot,\bot),(\top,\top),(\bot,?),(\top,?),(?,?)\}$.

We call a sequence $\sigma$ an open sequence if it is a sequence over open sets, i.e., $\sigma\in(\mathbb{N}\rightarrow 3^{\Sigma})$. For two open sequences $\sigma$ and $\sigma^{\prime}$ we define the partial order $\sqsubseteq$ such that $\sigma\sqsubseteq\sigma^{\prime}$ if for all $i\in\mathbb{N}$, $\sigma(i)\sqsubseteq\sigma^{\prime}(i)$. For a sequence $\sigma\in(\mathbb{N}\rightarrow 3^{\Sigma})$ and $\Sigma^{\prime}\subseteq\Sigma$ the sequence $\sigma_{\Sigma^{\prime}}\in(\mathbb{N}\rightarrow 3^{\Sigma^{\prime}})$ is the sequence where for all $i$, $\sigma_{\Sigma^{\prime}}(i)=\sigma(i)_{\Sigma^{\prime}}$.

We define the satisfaction relation of LTL over open sequences as follows. Given an LTL formula $\varphi$ over a set of atomic propositions $\textit{AP}=O\cup I$, an open sequence $\sigma$ satisfies $\varphi$, denoted by $\sigma\models\varphi$, if for each sequence $\sigma^{\prime}\in L(\varphi)$ that is input equivalent to $\sigma$, i.e., $\sigma_{I}=\sigma^{\prime}_{I}$, we have $\sigma^{\prime}\sqsubseteq\sigma$. For a fixed sequence of inputs $\varsigma\in(\mathbb{N}\rightarrow 2^{I})$, there is a unique open sequence $\sigma$ with $\sigma_{I}=\varsigma$ that satisfies $\varphi$ and that is minimial with respect to the partial order $\sqsubseteq$, i.e., for all sequences $\sigma^{\prime}\in(\mathbb{N}\rightarrow 3^{\textit{AP}})$ with $\sigma^{\prime}\models\varphi$ and $\sigma^{\prime}_{I}=\varsigma$, we have $\sigma\sqsubseteq\sigma^{\prime}$. We call such sequence a minimal satisfying sequence. For an LTL formula $\varphi$, we denote the set of all minimal satisfying sequences by $\min(\varphi)$.

Building on the definitions of open sequences and transition systems we introduce the notion of skeletons of reactive systems, which are transition systems labeled with open sets from $3^{O}$.

Definition 1 (Skeleton)

For a set $\textit{AP}=O\cup I$ of atomic propositions, a skeleton over AP is a $3^{O}$-labeled-$2^{I}$-transition system.

The language of a skeleton $\mathcal{S}$ is the set of open sequences given by the set of its traces. Figure 2 shows four skeletons defined over the sets $I=\{r_{1},r_{2}\}$ and $O=\{g_{1},g_{2}\}$. Figures 2 and 2 both define the language $\{\sigma:\mathbb{N}\rightarrow 3^{\textit{AP}}\mid\forall i.\sigma(i)(g_{1})=\sigma(i)(g_{2})=?\}$, i.e., for all input sequences the values of the output propositions $g_{1}$ and $g_{2}$ are open in all positions. The language of the skeleton in Figure 2 is the set $\{\sigma:\mathbb{N}\rightarrow 3^{\textit{AP}}\mid\sigma(0)(g_{1})=\sigma(0)(g_{2})=\bot,\forall i>0.~{}\sigma(i)(g_{1})=\top\wedge\sigma(i)(g_{2})=?\}$ where the values of $g_{1}$ are fixed in all positions and for $g_{2}$ only in the first position of the sequence.111Note that skeletons have no open values for input propositions.

We say that a skeleton $\mathcal{S}$ is a model of an LTL formula $\varphi$ denoted by $\mathcal{S}\models\varphi$, if $L(\mathcal{S})=\min(\varphi)$. Intuitively, for an LTL formula $\varphi$, a skeleton gives an incomplete transition system where values of atomic propositions that are not deterministically fixed by $\varphi$, are left open, i.e., they are mapped to the value $?$ in the open set of a state. Consider the formula $\varphi=\overline{g}_{1}\wedge\overline{g}_{2}\wedge\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(r_{1}\rightarrow\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}g_{1})$. We notice that all transition systems that satisfy $\varphi$ must have the label $\overline{g}_{1}\overline{g}_{2}$ in the initial state. For the rest of the transition system, the formula forces only to label a state with $g_{1}$ in case the direction(input) leading to this state contains the proposition $r_{1}$, and leaves it open on how to label the states reached by other directions, or whether to label a state with $g_{2}$ if it is reached by an input where $r_{1}$ is true (Figure 2).

Building on the satisfaction relation between LTL and skeleton we investigate in the next sections the problems of model checking and synthesis of skeletons.

4 Model Checking Skeletons

We present an automata-based model checking algorithm for skeletons. Given an LTL formula $\varphi$ we show that we can construct a nondeterministic Büchi automaton that recognizes the complement language $\overline{\min(\varphi)}$. Using the usual product construction, in this case, the product of the automaton and the skeleton, one can check whether the resulting automaton contains a path that simulates an accepting path in the nondeterministic automaton. If this is the case, then the language of the skeleton contains a sequence in $\overline{\min(\varphi)}$ and, thus, the skeleton is not a model for the formula $\varphi$. Using the construction of the product automaton we also show that checking whether a skeleton is a model of an LTL formula can be done in space exponential in the length of the formula.

Lemma 1

Given an LTL formula $\varphi$ we can build a nondeterministic Büchi automaton $\mathcal{N}=(3^{\textit{AP}},Q,q_{0},F,\delta)$ such that $L(\mathcal{N})=\overline{\min(\varphi)}$. The number of states of $\mathcal{N}$ is doubly-exponential in the length of $\varphi$.

Construction.

The language $\overline{\min(\varphi)}$ contains all sequences $\sigma:\mathbb{N}\rightarrow 3^{\textit{AP}}$ that are not minimal satisfying open sequences for $\varphi$. These can be distinguished by two types of open sequences. The first type involves sequences $\sigma$ where in some position $i$ the truth value of a proposition $p\in\textit{AP}$ is open (mapped to $?$), although, in all sequences $\sigma^{\prime}\in L(\varphi)$ with $\sigma_{I}=\sigma^{\prime}_{I}$ the proposition $p$ has the one same truth value (one of $\top$ or $\bot$ in all sequences) at position $i$. The second type are sequences $\sigma$, where in some position $i$ a proposition $p$ has truth value $\bot$(resp. $\top$), although, there exists another sequence $\sigma^{\prime}\in L(\varphi)$ with $\sigma^{\prime}_{I}=\sigma_{I}$ and $\sigma^{\prime}(i)(p)=\top$(resp. $\bot$). The latter case also subsumes the case of sequences $\sigma\in(\mathbb{N}\rightarrow 2^{\textit{AP}})$ with $\sigma\not\in L(\varphi)$.

We construct a Büchi automaton $\mathcal{N}=(3^{\textit{AP}},Q,q_{0},F,\delta)$ that accepts an open sequence $\sigma$ if and only if $\sigma\not\in\min(\varphi)$. The automaton is composed of two nondeterministic Büchi automata $\mathcal{N}_{1}=(3^{\textit{AP}},Q_{1},q_{0,1},F_{1},\delta_{1})$ and $\mathcal{N}_{2}=(3^{\textit{AP}},Q_{2},q_{0,2},F_{2},\delta_{2})$, one for each of the sequence types mentioned above. We define the automaton as $\mathcal{N}=\mathcal{N}_{1}\vee\mathcal{N}_{2}$, where $Q=\{q_{0}\}\cup Q_{1}\cup Q_{2}$, $F=F_{1}\cup F_{2}$ and $\delta=\{(q_{0},a,\delta_{1}(q_{0,1},a)\vee\delta_{2}(q_{0,2},a))\mid a\in 3^{\textit{AP}}\}\cup\delta_{1}\cup\delta_{2}$

Automaton $\mathcal{N}_{1}$ accepts a sequence $\sigma\in(\mathbb{N}\rightarrow 3^{\textit{AP}})$ if $\sigma$ has a position $i$ where an atomic proposition $p\in\textit{AP}$ is incorrectly marked as open. The automaton $\mathcal{N}_{1}$ can be constructed as follows:

Let $\mathcal{U}_{1}=(2^{\textit{AP}},Q_{1}^{\mathcal{U}},q_{0,1}^{\mathcal{U}},F_{1}^{\mathcal{U}},\delta_{1}^{\mathcal{U}})$ be a universal co-Büchi automaton for the formula $\neg\varphi$. We extend the automaton $\mathcal{U}_{1}$ to another universal co-Büchi automaton $\mathcal{U}_{1}^{*}$ over an extended alphabet $\{\top,\bot,?,*_{\top},*_{\bot}\}^{\textit{AP}}$. We make use of the values $*_{\top}$ and $*_{\bot}$ to encode in the input sequence whether a mapping to $?$ is wrong, and whether it is wrong when replacing $?$ by $\top$ or by $\bot$. We define $\mathcal{U}_{1}^{*}=(\{\top,\bot,?,*_{\top},*_{\bot}\}^{\textit{AP}},Q_{1}^{*},q_{0,1}^{*},F_{1}^{*},\delta_{1}^{*})$ over two copies of the automaton $\mathcal{U}_{1}$(denoted by the numbers 1 and 2) where $Q_{1}^{*}=Q_{1}^{\mathcal{U}}\times\{1,2\}$,  $q_{0,1}^{*}=(q_{0,1}^{\mathcal{U}},1)$,  $F_{1}^{*}=F_{1}^{\mathcal{U}}\times\{1,2\}$. The transition function $\delta_{1}^{*}$ is given by the union of the following sets:

• •

$\{((q,h),v,\delta_{1}^{\mathcal{U}}(q,v)_{\{q^{\prime}\in Q_{1}^{\mathcal{U}}/(q^{\prime},h)\}})\mid h\in\{1,2\},\forall p\in O.v(p)\in\{\top,\bot\}\}$

where in both copies of the automaton $\mathcal{U}_{1}$, transitions over symbols $v$ with no open values remain in the same copy and follow the structure of the transition relation $\delta_{1}^{\mathcal{U}}$ of $\mathcal{U}_{1}$. The operation $\{q^{\prime}\in Q_{1}^{\mathcal{U}}/(q^{\prime},h)\}$ substitutes every appearance of a state $q^{\prime}$ in $\delta_{1}^{\mathcal{U}}(q,v)$ by a state $(q^{\prime},h)$ from $Q_{1}^{*}$.

• •

$\{((q,h),v,(\delta_{1}^{\mathcal{U}}(q,v[p\mapsto\top])\wedge\delta_{1}^{\mathcal{U}}(q,v[p\mapsto\bot]))_{\{q^{\prime}\in Q_{1}^{\mathcal{U}}/(q^{\prime},h)\}})\mid\\ h\in\{1,2\},p\in O,v(p)=?,\}$

universal transitions for symbols where a proposition $p$ has an open truth value imitating transitions for both truth values $\top$ and $\bot$ for $p$.

• •

$\{((q,1),v,\delta_{1}^{\mathcal{U}}(q,v[p\mapsto\top])_{\{q^{\prime}\in Q_{1}^{\mathcal{U}}/(q^{\prime},2)\}})\mid p\in O,v(p)=*_{\top}\}$

when we guess at some position $i$ that an open truth value for a proposition $p$ is wrong, and it is wrong when replacing it by $\top$ we follow the transition $\top$ to the second copy of $\mathcal{U}_{1}$ in which $?,*_{\bot}$ and $*_{\top}$ are treated equivalently. This helps to check, whether replacing $?$ by $\top$ results in accpeting run in $\mathcal{U}_{1}$, which means that at position $i$ the truth value $\top$ violates the property $\varphi$, and thus it cannot be open at the that point.

• •

$\{((q,1),v,\delta_{1}^{\mathcal{U}}(q,v[p\mapsto\bot])_{\{q^{\prime}\in Q_{1}^{\mathcal{U}}/(q^{\prime},2)\}})\mid p\in O,v(p)=*_{\bot}\}$

which introduce transitions that involve the dual case of $*_{\top}$.

• •

$\{((q,2),v,(\delta_{1}^{\mathcal{U}}(q,v[p\mapsto\top])\wedge\delta_{1}^{*}(q,v[p\mapsto\bot]))_{\{q^{\prime}\in Q_{1}^{\mathcal{U}}/(q^{\prime},2)\}})\mid\\ p\in O,v(p)\in\{*_{\bot},*_{\top}\}\}$

these transitions make sure that when moving to copy 2 of $\mathcal{U}_{1}$, values $*_{\top}$ and $*_{\bot}$ are treated equally to $?$, because after guessing that a $?$ is wrong it must be wrong for all continuations.

In order to obtain the desired automaton $\mathcal{N}_{1}$ over the alphabet $3^{\textit{AP}}$ we first transform the automaton $\mathcal{U}_{1}^{*}$ to a nondeterministic automaton $\mathcal{N}_{1}^{*}$ with $L(\mathcal{U}_{1}^{*})=L(\mathcal{N}_{1}^{*})$ using a subset construction. This is necessary in order to merge all transitions $*_{\bot}$ at one level into one state. The same holds also for transitions $*_{\top}$. In this way, we can check whether at some position in a sequence a value $?$ is wrong by checking all possible branches of the automaton $\mathcal{U}_{1}^{*}$ at that level. The automaton $\mathcal{N}_{1}^{*}$ can be transformed now to the desired automaton $\mathcal{N}_{1}$ by projecting every transition label with values in $\{*_{\top},*_{\bot}\}$ to a label $v^{\prime}\in 3^{\textit{AP}}$ such that for every $p\in O$, if $v(p)=*_{\top}$ or $v(p)=*_{\bot}$ then $v^{\prime}(p)=?$.

The size of the automaton $\mathcal{U}_{1}$ is exponential in the length of $\varphi$ using the transformation of LTL formulas into alternating Büchi automata [17], and then using a subset construction. The transformation to $\mathcal{U}_{1}^{*}$ from $\mathcal{U}_{1}$, and to $\mathcal{N}_{1}$ from $\mathcal{N}_{1}^{*}$ are both polynomial, and exponential from $\mathcal{U}_{1}^{*}$ to $\mathcal{N}^{*}_{1}$. Thus, the size of $\mathcal{N}_{1}$ is doubly-exponential in the length of $\varphi$.

In a similar way, we can construct the automaton $\mathcal{N}_{2}$. Automaton $\mathcal{N}_{2}$ accepts a sequence $\sigma\in(\mathbb{N}\rightarrow 3^{\textit{AP}})$ if a proposition $p\in\textit{AP}$ is incorrectly mapped to $\top$ or $\bot$. Starting with the alternating Büchi automaton for the formula $\varphi$, we extend the alphabet with symbols $*_{\top}$ and $*_{\bot}$ and build an automaton $\mathcal{U}_{2}^{*}=(\{\top,\bot,?,*_{\top},*_{\bot}\}^{\textit{AP}},Q_{2}^{*},q_{0,2}^{*},F_{2}^{*},\delta_{2}^{*})$. Whenever we read a symbol $v$ where some $p\in O$ is mapped to $*_{\top}(*_{\bot})$, the automaton follows the transition for $v(p)=\bot(\top)$. After turning $\mathcal{U}_{2}^{*}$ to a nondeterministic automaton and projecting, a label $v$ is replaced by a label $v^{\prime}$ such that for every $p\in O$, if $v(p)=*_{\top}$ or $v(p)=*_{\bot}$ then $v^{\prime}(p)=\top$ or $v^{\prime}(p)=\bot$, respectively. The automaton $\mathcal{N}_{2}$ is doubly-exponential in the length of $\varphi$.

Proof

Let $\sigma\in(\mathbb{N}\rightarrow 3^{\textit{AP}})$. We distinguish three cases:

• •

$\sigma\in\overline{\min(\varphi)}$ and for some $i$ and some $p\in O$, the mapping $\sigma(i)(p)=?$ is wrong. We assume, w.l.o.g., that for all $\sigma^{\prime}\in L(\varphi)$ with $\sigma_{I}=\sigma^{\prime}_{I}$, that $\sigma^{\prime}(i)(p)=\top$, and that $i$ is the first position for which $\sigma(i)(p)=?$ is wrong. A run of the automaton $\mathcal{N}_{1}$ over $\sigma$ is a sequence $r\in(\mathbb{N}\rightarrow 2^{Q_{1}^{*}})$. Let $r=X_{0}X_{1}...$ be the run of the automaton $\mathcal{N}$ on $\sigma$, where $X_{0}=\{q_{0,1}^{*}\}$, and up to the position $i$ the run follows for each mapping to $?$ the transitions in $\mathcal{N}_{1}$ that were transitions for mappings to $?$ in the automaton $\mathcal{N}_{1}^{*}$ before the projection, i.e., all sets $X_{j}$ with $j\leq i$ contain only states $(q,1)$ from $Q_{1}^{*}$, where $q\in Q_{1}^{\mathcal{U}}$. In the position $i$, where the mapping to $?$ is incorrect, the run follows the transition with $?$ in state $X_{i}$ of $\mathcal{N}_{1}$ that can be mapped to a transition $*_{\bot}$ in the automaton $\mathcal{N}_{1}^{*}$ which moves to a set $X_{i+1}$ with only states $(q,2)$ from $Q_{1}^{*}$, i.e., the transition that checks whether replacing $?$ at $i$ with $\bot$ always leads to rejecting states for possible instantiations of upcoming $?$. As $\mathcal{U}_{1}^{*}$ is built from copies of the automaton $\mathcal{U}_{1}$ for the formula $\neg\varphi$, following the transition for $*_{\bot}$ means replacing at position $i$ the value $?$ with $\bot$, which can only lead to rejecting runs, because the automaton $\mathcal{U}_{1}$ accepts no sequence where $p$ is mapped to value $\bot$ at position $i$.

• •

$\sigma\in\overline{\min(\varphi)}$ and for some $i$ and some $p\in O$, $\sigma(i)(p)$ is incorrectly mapped to $\top$ or to $\bot$. With the same argumentation of the last case over the structure of the automaton $\mathcal{N}_{2}$ the claim can be proven.

• •

$\sigma\in\min(\varphi)$. In this case, for each position $i$, for each proposition $p\in O$ such that $\sigma(i)(p)=?$, and for each instantiation of $?$ for $p$ in position $i$, there are instantiations for all other $?$ values in $\sigma$ and for all propositions such that the resulting sequence $\sigma^{\prime}\in(\mathbb{N}\rightarrow 2^{\textit{AP}})$ is in $L(\varphi)$. Let $r=X_{0}X_{1}...$ be a run of $\mathcal{N}_{1}$ on $\sigma$. If $r$ follows all transitions for a mapping to $?$ that correspond to a transition for the value $?$ in $\mathcal{N}_{1}^{*}$. In this case, all sets $X_{j}$ for $j\geq 0$ have states $(q,1)$ of $\mathcal{U}_{1}^{*}$ where $q\in Q_{1}^{\mathcal{U}}$ and the run is not accepting, because the run simulates a universal run tree in $\mathcal{U}_{1}^{*}$ with at least one non-accepting branch, because there is an instantiation for $\sigma$ that is a model of $\varphi$. If at any point, then run $r$ takes a transition for some mapping to $?$ that corresponds to a transition $*_{\bot}$ or $*_{\top}$ in the automaton $\mathcal{N}_{1}^{*}$, then the run cannot be accepting, otherwise there is a mapping to $?$ for some proposition $p\in O$ in some position in $\sigma$ for which all other $?$ in $\sigma$ cannot be instantiated appropriately in order to get a model in $\sigma$.

In a similar way we can also prove that $\mathcal{N}_{2}$ has no accepting run for $\sigma$.

∎

To check whether a skeleton $\mathcal{S}$ is a model for a given LTL formula $\varphi$ we compute the product $\mathcal{P}=\mathcal{S}\times\mathcal{N}$ where $\mathcal{N}$ is nondeterministic Büchi automaton with $L(\mathcal{N})=\overline{\min(\varphi)}$ constructed in Lemma 1. If $\mathcal{P}$ contains a path that simulates an accepting path in $\mathcal{N}$, then $\mathcal{S}$ has a path that violates the property $\varphi$, i.e., there is a sequence in the language $L(\mathcal{S})$ that is not in $\min(\varphi)$.

Instead of constructing the product automaton $\mathcal{P}$ one can also guess a run in $\mathcal{P}$ and check whether it is accepting222This follows the idea of the Pspace model checking algorithm for LTL over transition systems [3]. Based on this idea, the complexity of model checking skeleton is given by the following theorem.

Theorem 4.1

Checking whether a skeleton $\mathcal{S}$ is a model for an LTL formula $\varphi$ is in Expspace.

5 Synthesis of Skeletons

For a set of atomic propositions $\textit{AP}=I\cup O$, to check whether there is $2^{O}$-labeled $2^{I}$-transition system $\mathcal{T}$ that satisfies a given LTL formula $\varphi$, one would construct a deterministic $\omega$-automaton $\mathcal{D}$ (for example a parity automaton) with $L(\mathcal{D})=L(\varphi)$, interpret the automaton as a tree automaton over trees with labels from $3^{O}$ and directions from $2^{I}$ and check its emptiness. In case, the language of the automaton is not empty the procedure returns a transition system $\mathcal{T}$ that models the formula $\varphi$. In the same fashion, we can construct a deterministic $\omega$-automaton for the language $\min(\varphi)$ (for example by determinizing the automaton from Lemma 1) and check whether there is a skeleton that is a model for $\varphi$ by performing an emptiness check over tree automaton interpretation of the deterministic automaton.

The deterministic automaton is very expensive to construct (triple exponential in the formula $\varphi$). Instead, we show that we can avoid this construction of the large deterministic automaton using learning. In comparison to transition systems, given an LTL formula, we show that it has a unique minimal skeleton that models the formula. The language of the skeleton is a safety language, and thus, can be characterized by a bad-prefix automaton, which is a finite word automaton. We use the learning algorithm L∗ to learn the deterministic bad-prefix automaton [2], which can be easily transformed to a skeleton that models the formula. The learning algorithm learns the skeleton in time polynomial in the size of the minimal skeleton.

5.1 Learning Skeletons

In the following we present an algorithm for learning skeletons of LTL formulas. Our algorithm is based on the $\text{L}^{*}$ algorithm for learning deterministic finite automata introduced by Dana Angluin [2]. The setting of the L∗ algorithm involves two key actors, the learner and the teacher. The learner tries to learn a language known to the teacher by learning a minimal deterministic finite word automaton for the language. The interaction between the learner and the teacher is driven by two types of queries: membership queries, where the learner asks whether a particular word is in the language, and equivalence queries, to check whether a learned deterministic finite automaton indeed defines the language to be learned. Here, the teacher responds either with a “yes” or with a counterexample, which is a word in the symmetric difference of the language of the learned automaton and the actual language. A teacher is called minimally adequate, if she can answer membership and equivalence queries.

Theorem 5.1

[2]* Given a minimally adequate Teacher for an unknown regular language $L$, we can construct a minimal finite word automaton that accepts $L$, in time polynomial in the number of states of the automaton and the length of the largest counterexample returned by the teacher.*

For an LTL formula $\varphi$ we show that the language of a skeleton that satisfies $\varphi$ is a safety language. This can be characterized by a language over finite words, namely the language of bad-prefixes. The L∗ algorithm can learn a finite automaton for the language of bad-prefixes, which in turn can then be transformed to a skeleton for the property $\varphi$.

Lemma 2

For an LTL formula $\varphi$, the language $\min(\varphi)$ is a safety language.

Proof

We show that every $\sigma\in\overline{\min(\varphi)}$ has a bad-prefix. We distinguish two cases for $\sigma$:

• •

There is a point $i$ in $\sigma$ and a proposition $p$ such that $\sigma(i)(p)=\top(\text{or }\bot)$ and there is a sequence $\sigma^{\prime}\in L(\varphi)$ with $\sigma_{I}=\sigma^{\prime}_{I}$ and $\sigma^{\prime}(i)(p)=\bot(\text{or}\top)$. Thus, any finite sequence $v_{0}\ldots v_{i}\in(3^{\textit{AP}})^{*}$ with $(v_{0}\ldots v_{i})_{I}=(\sigma(0)\ldots\sigma(i))_{I}$ and $v_{i}(p)\not=?$ is a bad-prefix for $\min(\varphi)$.

• •

There is a point $i$ in $\sigma$ and a proposition $p$ such that $\sigma(i)(p)=?$ and for all $\sigma^{\prime}\in L(\varphi)$ with $\sigma_{I}=\sigma^{\prime}_{I}$ we have $\sigma^{\prime}(i)(p)$ is solely $\top$ or solely $\bot$. In this case, every finite sequence $v_{0}\ldots v_{i}\in(3^{\textit{AP}})^{*}$ with $(v_{0}\ldots v_{i})_{I}=(\sigma(0)\ldots\sigma(i))_{I}$ and $v_{i}(p)=?$ is a bad-prefix for $\min(\varphi)$.

∎

From the last lemma we deduce, that a skeleton $\mathcal{S}$ for an LTL formula $\varphi$ can be seen as a safety automaton that accepts the language of minimal satisfying open sequences for $\varphi$. In particular, there is a bad-prefix automaton $\mathcal{B}$ that accepts the language of bad-prefixes of the language $\min(\varphi)$.

We use the L∗ algorithm to learn a deterministic bad-prefix automaton for the language $\min(\varphi)$. Figure 3 shows a high level flow graph of the learning algorithm333For more details on the L∗ algorithm we refer the reader to [2].. The learner poses a series of membership questions before making a conjecture about the bad-prefix automaton. With a membership query the learner asks whether a finite word $w\in(3^{\textit{AP}})^{*}$ is a bad-prefix for $\min(\varphi)$. If $w$ is a bad-prefix then the teacher returns yes, and no otherwise. The equivalence queries allow the learner to check whether a skeleton $\mathcal{S}$ is correct, i.e., $L(S)=\min(\varphi)$. The teacher either confirms the automaton or returns a counterexample to the learner. The latter is either a bad-prefix that is not rejected by $\mathcal{B}$ or word $w\in(3^{\textit{AP}})^{*}$ that is not a bad-prefix for $\min(\varphi)$ yet is in the language of $\mathcal{B}$. The black box shown in Figure 3 between the bad-prefix automaton and a skeleton, is a check whether the safety language characterized by the bad-prefix automaton can be represented by a skeleton. We will refer to this check as the output consistency check and will explain it later in more detail.

The skeleton returned by the learning procedure is minimal and it is unique.

Lemma 3

For each LTL formula $\varphi$ there is a unique (up to isomorphism) minimal skeleton $\mathcal{S}$ such that $\mathcal{S}\models\varphi$.

Proof

Let $\mathcal{S}=(S,s_{0},\tau,o)$ and $\mathcal{S}^{\prime}=(S^{\prime},s_{0}^{\prime},\tau^{\prime},o^{\prime})$ be two minimal skeletons for $\varphi$, i.e, $|S|=|S^{\prime}|=c$ and there is no skeleton $\mathcal{S}^{\prime\prime}=(S^{\prime\prime},s^{\prime\prime}_{0},\tau^{\prime\prime},o^{\prime\prime})$ for $\varphi$ with $|S^{\prime\prime}|<c$. We show that $\mathcal{S}$ and $\mathcal{S}^{\prime}$ define the same skeleton up to isomorphism. Let $\beta=\{(s,s^{\prime})\in S\times S^{\prime}~{}|~{}\forall\sigma_{I}\in(2^{I})^{*}.~{}\tau^{*}(s0,\sigma_{I})=s\leftrightarrow\tau^{\prime*}(s^{\prime}_{0},\sigma_{I})=s^{\prime}\}$. The relation $\beta$ is bijective because $\tau^{*}$ and $\tau^{\prime*}$ are both functional and complete. Thus, there is a one-to-one mapping between the states of $\mathcal{S}$ and those of $\mathcal{S}^{\prime}$, and for each $(s_{1},i,s_{2})\in\tau$ we have $(\beta(s_{1}),i,\beta(s_{2}))\in\tau^{\prime}$. For each $(s,s^{\prime})\in\beta$ it is also the case that $o(s)=o^{\prime}(s^{\prime})$, otherwise, there is an input sequence that distinguishes a trace in $\mathcal{S}$ from the corresponding one in $\mathcal{S}^{\prime}$, which contradicts the assumption that $L(\mathcal{S})=L(\mathcal{S}^{\prime})$. This implies that $\mathcal{S}$ is isomorphic to $\mathcal{S}^{\prime}$. ∎

In the next sections we show how membership and equivalence queries can be solved algorithmically.

5.2 Membership Queries

In this section we show that using the ideas of the automaton presented in Lemma 1 we can check whether a word is a bad-prefix in space exponential in the length of $\varphi$.

Theorem 5.2

Given an LTL formula $\varphi$ and a finite word $w\in(3^{\textit{AP}})^{*}$, checking whether $w$ is a bad-prefix for $\min(\varphi)$ is in Expspace.

Proof

A finite word $w\in(3^{\textit{AP}})^{*}$ is a bad-prefix for $\min(\varphi)$ if $w=w_{0}\dots w_{n}$ has a prefix and there is a sequence of input values $\varsigma$ and no sequence $\sigma:\mathbb{N}\rightarrow 3^{\textit{AP}}$ with $\sigma_{I}=\varsigma$ can extend $w$ to a sequence in $w\cdot\sigma\in\min(\varphi)$. Let $\mathcal{U}=(\Sigma,Q,q_{0},\delta,F)$ be a universal co-Büchi automaton such that $L(\mathcal{U})=L(\neg\varphi)$. The idea is to iteratively construct a run of the automaton $\mathcal{U}$ and check if the run is accepting (remember that a run of $\mathcal{U}$ is $Q$-tree). Given the input word $w$, we first guess which position $i$ of $w$ contains a wrong mapping and compute the set of states of the run tree over $w_{0}\dots w_{i}$ reached at this position. Then, we compute the set of states reached via choosing the transition for which the guessed position $i$ is wrong. Form here on, we guess the next input and branch universally for all valuations of the output propositions, and compute the next set of reached states. This is repeated $2^{|Q|}$ times (At latest at position $2^{|Q|}$ we reach a set of states, that was seen before and enter a loop in the run). If during the procedure a valid accepting configuration of the universal automaton was guessed, then we have found a sequence of inputs $\varsigma$ for which no $\sigma$ with $\sigma_{I}=\varsigma$ extends the prefix of $w_{0}\dots w_{i}$ to a sequence in $\min(\varphi)$. Thus, $w$ is a bad-prefix for $\min(\varphi)$. In each step we only need to remember the currently reached set of states of $\mathcal{U}$, and whether we have seen an accepting configuration of $\mathcal{U}$. Furthermore, the number of iteration can be encoded in binary and is polynomial in the size of $\mathcal{U}$, which in turn is exponential in the length of $\varphi$. ∎

5.3 Equivalence Queries

We move now to equivalence queries. To check whether a skeleton is a model for a formula $\varphi$ we apply the model checking algorithm presented in Section 4. The learning algorithm first constructs a bad-prefix automaton for the language $\min(\varphi)$. We show that this automaton can be turned into a safety automaton for $\min(\varphi)$ on which we can simulate a skeleton for $\varphi$. In case we cannot simulate the skeleton on top of the safety automaton, then there is no skeleton that models the formula $\varphi$.

Lemma 4

Given a deterministic bad-prefix automaton $\mathcal{B}$ for a safety property $\varphi$, we can construct a deterministic safety automaton $\mathcal{S}$ for $\varphi$ in time linear in the size of $\mathcal{B}$.

Construction.

Let $\mathcal{B}=(\Sigma,Q,q_{0},F,\delta)$ be a bad-prefix automaton for some property $\varphi$ and we assume it is complete. We construct a safety automaton $\mathcal{S}=(\Sigma,Q^{\prime},q_{0}^{\prime},\delta^{\prime})$ for $\varphi$ by first removing all states in $F$ and then by iteratively removing all resulting sink states in the automaton.

Remark 1

Note that if $\mathcal{B}$ is minimal, so is $\mathcal{S}$.

Before we move on to the construction we consider following fact about skeletons and the language $\min(\varphi)$ for some formula $\varphi$. Let $\textit{AP}=O\cup I$ be the set of atomic propositions. Let $\mathcal{S}=(S,s_{0},\tau,o)$ be a skeleton that models the formula $\varphi$. Let $\pi_{1}=(s_{0},i_{1})(s_{1},i_{1})\dots$ and $\pi_{2}=(s_{0},i_{1})(s_{1},i_{2})\dots$ be paths in $\mathcal{S}$ where $s_{0},s_{1}\in S$ and $i_{1},i_{2}\in I$. Then, both sequences $\sigma_{\pi_{1}}=(o(s_{0})\cup i_{1})(o(s_{1})\cup i_{1})\dots$ and $\sigma_{\pi_{2}}=(o(s_{0})\cup i_{1})(o(s_{1})\cup i_{2})\dots$, must be in the set $\min(\varphi)$, otherwise $\mathcal{S}$ is not a model of $\varphi$. This means, if the language $\min(\varphi)$ contains sequences $(o_{1}\cup i_{1})(o_{2}\cup i_{1})\dots$ and $(o_{1}\cup i_{1})(o^{\prime}_{2}\cup i_{2})\dots$ with $o_{2}\not=o^{\prime}_{2}$ then there is no skeleton that models $\varphi$, because $\min(\varphi)=L(\mathcal{S})$ and both traces cannot be trace of the skeleton at the same time.

Definition 2 (Output Consistent)

For a set of atomic propositions $\textit{AP}=O\cup I$, a safety automaton $\mathcal{A}=(3^{\textit{AP}},Q,q_{0},\delta)$ is output consistent, if for each state $q\in Q$ there is a unique mapping $v\in\{\bot,\top,?\}^{O}$ and for all transitions $(q,v^{\prime},q^{\prime})\in\delta$, $v^{\prime}(p)=v(p)$ for all propositions $p\in O$.

Lemma 5

Given an LTL formula $\varphi$, if there is an output consistent safety automaton $\mathcal{A}$ for the language $\min(\varphi)$, we can transform $\mathcal{A}$ to skeleton $\mathcal{S}$ that models $\varphi$. The size of $\mathcal{S}$ is equal to the size of $\mathcal{A}$.

Construction.

Let $\varphi$ be an LTL formula and let $\mathcal{A}=(3^{\textit{AP}},Q,q_{0},\delta)$ be an output consistent safety automaton for the language $\min(\varphi)$ constructed from a deterministic bad-prefix automaton as in Lemma 4. Let $Q=\{q_{0},q_{1}\dots q_{n}\}$. We can construct a skeleton $\mathcal{S}=(S,s_{0},\tau,o)$, where $S=\{s_{0},\dots,s_{n}\}$ and $o(s_{i})=X\cap O$ for $(q_{i},X,q^{\prime})\in\delta$ for some $q^{\prime}\in Q$, and $(s_{i},Y,s_{j})\in\tau$ for $Y\subseteq I$ when $(q_{i},o(s_{i})\cup Y,q_{j})\in\delta$. The skeleton $\mathcal{S}$ models $\varphi$, because it simulates the language of $\mathcal{A}$.

Lemma 6

Given a formula $\varphi$, if an output consistent safety automaton $\mathcal{A}$ with $L(\mathcal{A})=\min(\varphi)$ is minimal then the skeleton $\mathcal{S}$ extracted form $\mathcal{A}$ is also minimal.

Proof

This follows from the fact that we can use the reverse of the construction presented in Lemma 5 to construct the safety automaton from the skeleton. Assume $\mathcal{S}$ was not minimal, then there is a skeleton $\mathcal{S}^{\prime}$ with less number of states. This one, however, can be transformed backwards to a output consistent automaton of same size, which contradicts the assumption. ∎

Once we obtain a candidate skeleton, we check whether the skeleton is a model of the formula using the model checking algorithm presented in Section 4. If the skeleton is not a model, the algorithm returns a counterexample, which is a lasso-shaped trace in the candidate skeleton. As this trace must contain a bad-prefix, we can iteratively check all prefixes of the trace using membership queries until we reach the (shortest) bad-prefix.

Using the results presented in Theorem 4.1 (Equivalence query checking is in Expspace), Theorem 5.1 (L∗ learns a minimal bad-prefix automaton in polynomial time in the size of the minimal automaton), Theorem 5.2 (Membership checking is in Expspace), Lemma 2 (The language $\min(\varphi)$ can be characterized by a finite automaton), Lemma 3 (The minimal skeleton is unique), Lemma 5 (The safety automaton is a skeleton), and Lemma 6, we can conclude now with following theorem.

Theorem 5.3

Given an LTL formula $\varphi$, we can construct a skeleton $\mathcal{S}$ that models $\varphi$ in time polynomial in the size of the minimal skeleton of $\varphi$.

6 Conclusion

We have presented an analysis technique for temporal specifications of reactive systems that identifies, on the level of individual system outputs over time, which parts of the implementation are determined by the specification, and which parts are still open. Based on the algorithms developed in this paper, a synthesis tool can represent this information in the form of a skeleton for the reactive system. Skeletons are more informative than conventional transition systems in identifying critical situations that are still underspecified.

Our automaton-based model checking algorithm for skeletons also serves as the teaching oracle in the learning-based synthesis algorithm. The learning algorithm L∗ can be used to synthesize minimal skeletons because skeletons define safety languages, which can be characterized by a unique minimal bad-prefix automaton. Once the automaton is learned, it can directly be transformed into a skeleton for the specification. The skeleton is minimal and can be constructed in time polynomial in the number of states of the skeleton.

In the development of a reactive system, skeletons can be seen as an intermediate step between the specification of the system and its implementation. In future work, we plan to investigate this aspect further, by exploring an incremental development process, where the refinement of the specification is guided by the identification of underspecified situations through the skeletons synthesized from the intermediate specifications.