30 Years of Modal Transition Systems: Survey of Extensions and Analysis

Abstract

We survey the specification formalism of modal transition systems (MTS). We discuss various extensions of MTS, their relationships and modelling capabilities. The extensions include more involved modalities, quantitative aspects, or infinite state spaces. Further, we discuss problems arising in verification and analysis of these systems. We cover refinement checking, model checking and synthesis, standard logical and structural operations as used in specification theories as well as the respective tool support.

1 Introduction

Correctness of complex systems can be ensured in various ways. The key idea of verification is to first specify a property the system under development should satisfy and then to verify that this is indeed the case. An alternative to verification is refinement of the original specification into an implementation, which is guaranteed to satisfy the specification, for the refinement is designed to preserve the properties of interest. The refinement can be done either in one step, where the implementation is synthesized from the specification, or in more steps in a process of stepwise refinement. The latter is particularly useful when some details of the requirements are not known at the beginning of the design process, or synthesis of the whole system is infeasible, or in the component-based design where other systems can be reused as parts of the new system.

The difference between verifying and refining systems is reflected in two fundamentally different approaches to specifications. Firstly, the logical approach, relying on model checking algorithms, makes use of specifications given as formulae of temporal or modal logics. Secondly, the behavioural approach, relying on refinement, requires specifications to be given in the same formalism as implementations, e.g. a kind of a machine with an operational interpretation. We focus on the latter.

Example 1

Consider the scenario of developing a piece of software illustrated in Fig. 1. We start with a viewpoint $V_1$ on the system, e.g. the client’s view on the service functionality. This gets iteratively refined into a more concrete description $V_m$. Further, assume there is also another viewpoint $W_1$, e.g. a description of the service from the server point of view, which is refined in a similar fashion resulting in $W_n$. After these viewpoints are precise enough (although still very underspecified), we merge them into one, say S, using an operation of conjunction. The complete description is now modelled by S, which is to be implemented. Suppose we have components C and D at our disposal, which perform subroutines needed in S. We put C and D together into a component T using an operation of parallel composition. What remains to be designed is a component X that we can compose with T in parallel so that the result conforms to the specification S. The most general such X is called the quotient of S by T. Once we have X we can further refine the underspecified behaviour in any desired way resulting in a specification Y. The final step is to automatically synthesize an implementation Z that, for instance, satisfies additional temporal logic constraints $\varphi$ and/or is the cheapest implementation with respect to specified costs $\mathfrak C$. Specification theories [Lar90, BDH+12] are mathematical formalisms allowing for such development in a rigorous way.    $\triangle$

Fig. 1.

An example of a component-based step-wise design scheme

A good specification theory should (i) allow for all the operations mentioned in the example and efficient algorithms to compute them. Moreover, it should (ii) be expressive enough to allow for convenient modelling. The behavioural formalism of modal transition systems (MTS) [LT88] provides a convenient basis for such a theory and has attracted a lot of attention. Unfortunately, it does not satisfy either of the two stipulations above completely. In this paper, we survey extensions of MTS that meet all these demands and efficient algorithms for their analysis such as the mentioned operations, refinements, verification and synthesis. Further, we discuss a link between the MTS extensions and logics, thus building a bridge between the behavioural and the logical world, allowing us to combine them, enjoying the best of both worlds.

1.1 History of Modal Transition Systems

Modal transition systems (MTS) were introduced by Larsen and Thomsen [LT88] three decades ago. The goal was to obtain an expressive specification formalism with operational interpretation, allowing for refinement. The main advantage of MTS is that they are a simple extension of labelled transition systems, which have proved appropriate for behavioural description of systems as well as their compositions.

MTS consist of a set of states and two transition relations. The must transitions prescribe what behaviour has to be present in every refinement of the system; the may transitions describe the behaviour that is allowed, but need not be realized in the refinements. This allows us to underspecify non-critical behaviour in the early stages of design, focusing on the main properties, verifying them and sorting out the details of the yet unimplemented non-critical behaviour later.

Example 2

An MTS specification of a coffee machine is displayed in Fig. 2 on the left. May transitions are depicted using dashed arrows, must transitions using solid arrows. In the left state, the machine can either start to $\mathsf {clean}$ or accept a $\mathsf {coin}$. It may not always be possible to take the $\mathsf {coin}$ action, but if we do so the machine must offer $\mathsf {coffee}$ and possibly supplement the choice with $\mathsf {tea}$. An implementation of this specification is displayed on the right. Here the $\mathsf {clean}$ is scheduled regularly after every two beverages. In addition, $\mathsf {tea}$ can always be chosen instead of $\mathsf {coffee}$.    $\triangle$

Fig. 2.

An MTS specification and its implementation

The formalism of MTS has proven to be useful, most importantly in compositional reasoning and component-based design. Industrial applications are as old as [Bru97] where MTS have found use for an air-traffic system at Heathrow airport. Besides, MTS are advocated as an appropriate base for interface theories in [AHL+08a, RBB+09b, RBB+09a, RBB+11] and for product line theories in [LNW07a, Nym08, tBDG+15, tBFGM16, DSMB16]. Further, MTS-based software engineering methodology for design via merging partial descriptions of behaviour has been established in [UC04, BCU06, UBC07] and using residuation in [Rac07, Rac08, Ben08]. The theory found its applications also in testing [BDH+15, LML15]. MTS are used for program analysis using abstraction [GHJ01, DGG97, Nam03, DN04, dAGJ04, NNN08, CGLT09, GNRT10]. MTS specification formalisms are supported by several tools [DFFU07, BML11, KS13a, VR14].

Over the years, many extensions of MTS have been proposed. While MTS can only specify whether or not a particular transition is required, some extensions equip MTS with more general abilities to describe what combinations of transitions are possible. For instance, disjunctive MTS (DMTS) [LX90] can specify that at least one of a given set of transitions is present. One-selecting MTS [FS08] specify that exactly one of them is present. Acceptance automata [Rac07] can even express any Boolean combination of transitions, but only for deterministic systems. In all the mentioned cases, every must transition is also automatically a may transition, modelling that whatever is required is also allowed. Sometimes this assumption is dropped and the two transition relations are given independently, giving rise to mixed transition systems (MixTS) [DGG97, AHL+08b].

These formalisms have also been studied under other names in different contexts. To some extent equivalent variations of MTS have been adapted for model-checking: Kripke modal transition systems (KMTS) [HJS01], partial Kripke structures [BG00], and 3-valued Kripke structures [CDEG03]. In the same manner MixTS correspond to Belnap transition systems [GWC06a]. Further, DMTS correspond to generalized KMTS [SG04] or abstract transition systems [dAGJ04]. While the variants of MTS and MixTS have been used in practical symbolic model-checkers (e.g. [CDEG03, GC06, GWC06b]), the “hypermust” transitions in DMTS are hard to encode efficiently into BDDs. A comparison of usability of these systems for symbolic model checking can be found in [WGC09]. Acceptance automata were also studied as acceptance trees [Hen85].

1.2 Outline of the Paper

Section 2 introduces modal transition systems formally, recalls several logics used later, and explains the stipulations on good specification formalisms. Section 3 discusses extensions of MTS with respect to specifying the combinations of present transitions. Section 4 discusses extensions of MTS with respect to the underlying graph structure of the MTS, focusing on weighted graphs and infinite graphs. In Sect. 5, results on refinements, operations, implementation synthesis, and the available tools are surveyed. Section 7 concludes and mentions several possible future directions.

1.3 Further Sources

This survey is an updated adaptation of the author’s thesis [Kře14]. An excellent overview, however older, is provided in [AHL+08a]. Particular topics are explained in depth in several theses, e.g. applications to interface and product-line theories [Nym08], or extensions of MTS such as acceptance automata [Rac07], disjunctive MTS [Ben12], MTS under different semantics [Fis12], in quantitative settings [Juh13], with data [Bau12], or parameters and synchronization [Møl13].

2 Preliminaries

2.1 Modal Transition Systems

The original modal transition systems were introduced in [LT88] as follows, where $\varSigma$ is an action alphabet.

Definition 1

(Modal transition system). A modal transition system (MTS) is a triple $(P,\mathord {\mathop {\dashrightarrow }\limits ^{}},\mathord {\mathop {\longrightarrow }\limits ^{}})$, where P is a set of processes and $\mathord {\mathop {\longrightarrow }\limits ^{}}\subseteq \mathord {\mathop {\dashrightarrow }\limits ^{}}\subseteq P\times \varSigma \times P$ are must and may transition relations, respectively.

The must and may transitions capture the required and allowed behaviour, as discussed in the introduction. The most fundamental notion of the theory of modal transition systems is the modal refinement. Intuitively, a process s refines a process t if s concretizes t (or in other words, t is more abstract than s). Since processes are meant to serve as specifications, this is defined by (i) only allowing in s what is already allowed in t and (ii) requiring in s what is already required in t.

Definition 2

(Modal refinement). Let $(P_1,\mathord {\mathop {\dashrightarrow }\limits ^{}}_1,\mathord {\mathop {\longrightarrow }\limits ^{}}_1),\ (P_2,\mathord {\mathop {\dashrightarrow }\limits ^{}}_2,\mathord {\mathop {\longrightarrow }\limits ^{}}_2)$ be MTS and $s\in P_1, t\in P_2$ be processes. We say that s modally refines t, written $s\le _mt$, if there is a refinement relation $R\subseteq P_1\times P_2$ satisfying $(s,t)\in R$ and for every $(p,q)\in R$ and every $a \in \varSigma$:

• 1. if $p\mathop {\dashrightarrow }\limits ^{a}_{1}p'$ then there is a transition $q\mathop {\dashrightarrow }\limits ^{a}_{2}q'$ such that $(p',q')\in R$, and

• 2. if $q\mathop {\longrightarrow }\limits ^{a}_{2}q'$ then there is a transition $p\mathop {\longrightarrow }\limits ^{a}_{1}p'$ such that $(p',q')\in R$.

Example 3

In the course of the refinement process, must transitions are preserved, may transitions can turn into must transitions or disappear, and no new transitions are added. Note that refinement is a more complex notion than that of subgraph. Indeed, the same transition can be refined in different ways in different places as illustrated in Fig. 3.    $\triangle$

Fig. 3.

The refinement $i\le _ms$ is witnessed by the refinement relation $\{(i,s),(j_1,t),(j_2,t),(k_1,s),(k_2,s),(\ell ,t)\}$. Note that whenever there is a must transition in an MTS, we do not depict its underlying may transitions. Moreover, when a designated process of an MTS is considered initial, it is depicted with an incoming arrow.

Whenever $s\le _mt$, we call s a refinement of t and t an abstraction of s. We often consider MTS with a designated initial process; in such a case we say that an MTS refines another one if this is true of their initial processes.

One may refine MTS in a stepwise manner until $\mathord {\mathop {\dashrightarrow }\limits ^{}}=\mathord {\mathop {\longrightarrow }\limits ^{}}$ is obtained and no further refinement is possible. MTS with $\mathord {\mathop {\dashrightarrow }\limits ^{}}=\mathord {\mathop {\longrightarrow }\limits ^{}}$ are called implementations and can be considered as the standard labelled transition systems (LTS). Given a process s we denote by $\llbracket {s}\rrbracket =\{i\mid i \text { is an implementation and } i\le _ms\}$ the set of all implementations of s.¹ In the previous example, $j_1$ is not an implementation, while $j_2$ is considered an implementation since all reachable transitions satisfy the requirement. Further notice that $k_2\in \llbracket {s}\rrbracket$.

Note that on implementations the refinement coincides with the strong bisimilarity, and on modal transition systems without any must transitions it corresponds to the simulation preorder. Further, the refinement has a respective game characterization [BKLS09b] similar to (bi)simulation games.

2.2 Logics

A set of implementations can be specified not only by a behavioural specification such as an MTS, but also by a formula of a logic. Here we briefly recall two logics: $\mu$-calculus [Koz83] and LTL [Pnu77]. Let Ap be a set of atomic propositions.

${\varvec{\mu }}$ -calculus is given by the syntax

$$\begin{aligned} \varphi \,{:}{:}{=}\, \mathbf {tt}\mid \mathbf {ff}\mid p \mid \lnot p \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid [a]\varphi \mid \langle a\rangle \varphi \mid \mu X. \varphi \mid \nu X. \varphi \end{aligned}$$

where p ranges over Ap, a over $\varSigma$, and X over a set $Var$ of variables. We call $\mu$ the least fixpoint and $\nu$ the greatest fixpoint.

Linear temporal logic (LTL) is given by the syntax

$$\begin{aligned} \varphi \,{:}{:}{=}\,\mathbf {tt}\mid \mathbf {ff}\mid p \mid \lnot p \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid \mathbf {X}\varphi \mid \mathbf {X}_a \varphi \mid \mathbf {F}\varphi \mid \mathbf {G}\varphi \mid \varphi \mathbf {U}\varphi \end{aligned}$$

where p ranges over Ap and a over $\varSigma$. Given an implementation $(P,\mathord {\mathop {\longrightarrow }\limits ^{}})$ and a valuation $\nu :P\rightarrow 2^{Ap}$ over its state space, any run (maximal path in the directed graph of the LTS) induces a sequence from $(2^{Ap}\times \varSigma )^\mathbb N$ capturing the labelling of the visited processes and the actions taken there. The semantics here is a mixture of state-based and action-based properties:² given a sequence $\alpha _0 a_0 w$ we define $\alpha _0 a_0 w\models \mathbf {X}\varphi$ iff $w\models \varphi$; besides, $\alpha _0 a_0 w\models \mathbf {X}_a\varphi$ iff $w\models \varphi$ and $a=a_0$. The semantics of other operators is standard. An LTS satisfies $\varphi$ if all runs from its initial process satisfy $\varphi$.

Example 4

Consider the LTS and its valuation depicted in Fig. 4. While it satisfies $\mathbf {G}p$ and $\nu X.p\wedge [a]X$, it does satisfy neither $\mathbf {F}q$ nor $\mu X.q\vee [a]X$ due to the run looping in s.    $\triangle$

Fig. 4.

An LTS with a valuation $\nu$

2.3 Specification Theories

In order to support component based development, many specification theories have been designed. One usually requires existence and effective computability of several operations subject to various axioms. In the following, let s and t be processes, arguments of the operations.

Some operations are structural, stemming from the nature of behavioural descriptions, such as the operations of parallel composition and quotient. The parallel composition $\parallel$ should satisfy

• (parallel) for any processes x and $y, x\parallel y\le _ms\parallel t$ if $x\le _ms$ and $y\le _mt$,

called independent implementability. The quotient is an adjoint to parallel composition, hence the quotient $s/t$ of s by t should satisfy

• (quotient) for any process $x, x\le _ms/t$ if and only if $t\parallel x\le _ms$.

Given a specification s of the whole system and t of its component, the quotient $s /t$ is thus a compact description of all systems that can be put in parallel with t to get a system complying with s.

Other operations are inherited from the logical view, such as Boolean operations. A conjunction of two systems is the most general refinement of the two systems. As the greatest lower bound with respect to $\le _m$ it must satisfy

• (conjunction) for any process $x, x\le _ms\wedge t$ if and only if $x\le _ms$ and $x\le _mt$.

A bit weaker notion is that of consistency relation: a set of systems is consistent if they have a common implementation, i.e. if their conjunction has a non-empty set of implementations. Dually, one can define disjunction by requiring

• (disjunction) for any process $x, s\vee t \le _mx$ if and only if $s\le _mx$ and $t\le _mx$.

The remaining Boolean operation is that of complement:

• (complement) for any process $x, x\le _m{\bar{s}}$ if and only if $x\not \le _ms$.

For the related notion of difference, see e.g. [SCU11].

It is often not possible to satisfy all axioms in this strong form. For instance, automata-based specification formalisms are sometimes too weak to express the complement, which is the case also for MTS. Besides, the “complete specification theories” of [BDH+12] only require (parallel) in the above-mentioned “if” form. The other desired direction cannot in general be achieved in MTS [HL89, BKLS09b], see Fig. 5. Further, according to [BDH+12], existence of quotients and conjunctions is required if they have non-empty set of implementations. Here we presented a simpler version of the operator requirements, which is equivalent when MTS are enriched with the “inconsistent” specification with no implementations.

Fig. 5.

$i \le _ms_1 \parallel s_2$, but i cannot be written as $i_1\parallel i_2$ for any $i_1\le _ms_1,i_2\le _ms_2$

3 Extensions of Modalities

Since the modelling capabilities of basic MTS are quite limited, many extensions have appeared in the literature. In this section, we focus on extensions of the may and must transition relations. Standard MTS have two transition relations $\mathord {\mathop {\longrightarrow }\limits ^{}},\mathord {\mathop {\dashrightarrow }\limits ^{}}\subseteq P\times \varSigma \times P$ satisfying $\mathord {\mathop {\longrightarrow }\limits ^{}}\subseteq \mathord {\mathop {\dashrightarrow }\limits ^{}}$, which is called the syntactic consistency requirement. If this requirement is not imposed we obtain mixed transition systems as introduced in [DGG97].

Definition 3

(Mixed transition system). A mixed transition system (MixTS) over an action alphabet $\varSigma$ is a triple $(P,\mathord {\mathop {\dashrightarrow }\limits ^{}},\mathord {\mathop {\longrightarrow }\limits ^{}})$, where P is a set of processes and $\mathord {\mathop {\longrightarrow }\limits ^{}},\mathord {\mathop {\dashrightarrow }\limits ^{}}\subseteq P\times \varSigma \times P$ are must and may transition relations, respectively.

This extension allows us not only to have inconsistent specifications, but also a certain form of enforced non-deterministic choice:

Example 5

The specification of Fig. 6 requires an a transition followed by either only b’s or only c’s. Indeed, the must transition under a enforces a transition, but does not automatically allow it; only the two may transitions under a are allowed.    $\triangle$

Fig. 6.

A mixed transition system. Since must transitions are not necessarily also may transitions in MixTS, we depict may transitions explicitly for mixed systems here, even when there is a corresponding must transition.

Nevertheless, even this feature is often insufficient to specify which combinations of transitions can be implemented.

Example 6

Figure 7 on the left depicts an MTS that specifies the following. A $\mathsf {request}$ from a client may arrive. Then we can $\mathsf {process}$ it directly on the server or make a $\mathsf {query}$ to a database where we are guaranteed an $\mathsf {answer}$. In both cases we send a $\mathsf {response}$.

Fig. 7.

A potentially deadlocking s and two of its implementations $i_1,i_2$

An MTS can be refined in two ways: a may transition is either implemented (and becomes a must transition) or omitted (and disappears as a transition). On the right of Fig. 7 there is an implementation $i_1$ of the system, where the $\mathsf {process}$ing branch is implemented and the database $\mathsf {query}$ branch is omitted. Similarly, there is also an implementation omitting the $\mathsf {process}$ branch and implementing only the $\mathsf {query}$. However, there is also an undesirable implementation $i_2$ that does not implement any option and deadlocks as seen on the right of Fig. 7.    $\triangle$

To avoid deadlocking, we want to specify that either processing or query will be implemented. This is possible in disjunctive modal transition systems [LX90]. They were actually introduced as natural means for solutions to process equations since they can express both conjunctions and disjunctions of properties.

Definition 4

(Disjunctive modal transition system). A disjunctive modal transition system (DMTS) is a triple $(P,\mathord {\mathop {\dashrightarrow }\limits ^{}},\mathord {\mathop {\longrightarrow }\limits ^{}})$, where P is a set of processes and $\mathord {\mathop {\dashrightarrow }\limits ^{}}\subseteq P\times \varSigma \times P$ is the may and $\mathord {\mathop {\longrightarrow }\limits ^{}}\subseteq P\times 2^{\varSigma \times P}$ the must (or hyper-must) transition relation.

Example 7

Intuitively, in DMTS we can enforce a choice between arbitrary transitions, not just with the same action as in Example 5. Instead of forcing a particular transition, a must transition in DMTS specifies a whole set of transitions at least one of which must be present in any refinement. In our example, it would be the set consisting of processing and query transitions, see Fig. 8.    $\triangle$

Fig. 8.

A disjunctive modal transition system

Note that DMTS are capable of forcing any positive Boolean combination of transitions, simply by turning it into the conjunctive normal form. If the choice is supposed to be exclusive, we can use one-selecting MTS (1MTS) introduced in [FS08] with the property that exactly one transition from the set must be present. In 1MTS and also in underspecified transition systems (UTS) [FS05], both (hyper)must and (hyper)may transition relations are subsets of $P\times 2^{\varSigma \times P}$. For UTS, the syntactic consistency is required, i.e. the hyper-may is larger than the hyper-must.

Finally, explicit listing of all allowed combinations of outgoing transitions is used in acceptance automata [Rac08]. However, the language-theoretic definition is limited to deterministic systems.

Definition 5

(Acceptance automaton). An acceptance automaton (AA) is a pair $(P, PossibleTranSets )$, where P is a prefix-closed language over $\varSigma$ and $PossibleTranSets :P\rightarrow 2^{2^\varSigma }{\setminus }\emptyset$ satisfies the consistency condition: $wa\in P$ if and only if $a\in TranSet \in PossibleTranSets (w)$ for some $TranSet$.

Nevertheless, as the following example shows, convenient modelling requires even more features such as conditional or persistent choices.

Example 8

Consider a simple specification of a traffic light controller for several national variants for vehicles as well as for pedestrians, displayed on the right of Fig. 9. At any moment it is in one of the four states $red$, $green$, $yellow$ or $yellowRed$. The intuitive requirements are: if $green$ is on then the traffic light may either change to $red$ or $yellow$, and if it turned $yellow$ (as for vehicles) it must go to $red$ afterwards; if $red$ is on then it may either turn to $green$ (as for pedestrians and also for vehicles in some countries) or $yellowRed$, and if it turns $yellowRed$ it must go to $green$ afterwards.

However, these requirements (expressible as MTS) allow for three different undesirable implementations: (i) the light is constantly $green$, (ii) the lights switch non-deterministically, (iii) the lights switch deterministically, but $yellow$ is only displayed sometimes (e.g. every other time). While the first problem can be avoided using the choice in DMTS, the latter two cannot. To eliminate the second implementation, one needs an exclusive choice, as in 1MTS; for the third implementation to be removed, one needs a persistent choice. These can be modelled in parametric MTS [BKL+11, BKL+15] where a parameter describes whether and when the yellow light is used, making the choices permanent in the whole implementation. Additionally, the dependence on the parameter allows for modelling a conditional choice. Indeed, as illustrated in the middle of Fig. 9, depending on the value of another parameter, the yellow light can be consistently used or skipped in both phases.    $\triangle$

Definition 6

(Parametric modal transition system). A parametric MTS (PMTS) is a tuple $(P,\mathord {\mathop {\dashrightarrow }\limits ^{}}, Par ,\varPhi )$ where P is a set of processes, $\mathord {\mathop {\dashrightarrow }\limits ^{}}\subseteq P \times \varSigma \times P$ is a transition relation, Par is a finite set of parameters, and $\varPhi : P \rightarrow \mathcal Bool\mathcal Exp((\varSigma \times P) \cup Par )$ is an obligation function assigning to each process a Boolean expression over outgoing transitions and parameters.

These systems are “mixed”; a syntactic consistency $\forall s\in P:\forall (a,t) \in \varPhi (s):s\mathop {\dashrightarrow }\limits ^{a}t$ may be additionally required, making them “pure”. Intuitively, a set S of transitions from s is allowed if $\varPhi (s)$ is true under the valuation induced by S and the fixed parameters; for an example see Fig. 9. A PMTS is

• Boolean MTS (BMTS) [BKL+11] if it is parameter-free, i.e. if $Par = \emptyset$,

• transition system with obligation (OTS) [BK10] if it is BMTS and only parameters can be negated,

• DMTS is an OTS with $\varPhi (s)$ in the conjunctive normal form for all $s \in P$, DMTS is considered both mixed [LX90] and pure [BČK11],

• MixTS is a DMTS with $\varPhi (s)$ being a conjunction of positive literals (transitions) for all $s \in P$ (and the syntactic consistency not required),

• MTS is a MixTS with the and the syntactic consistency required,

• LTS is an MTS with $\varPhi (s) = \bigwedge T(s)$ for all $s \in P$, where $T(s) = \{(a,t) \mid s\mathop {\dashrightarrow }\limits ^{a}t\}$ is the set of all outgoing transitions of s.

Fig. 9.

Examples of PMTS and their modal refinement (Color figure online)

Fig. 10.

The syntactic hierarchy of MTS extensions (on the left) and the semantic one, not considering empty specifications (on the right)

The modal refinement over BMTS is an expected extension of that for MTS. Technically, let $\mathrm {Tran}(s) = \{ E \subseteq T(s) \mid E \models \varPhi (s)\}$ be the set of all admissible sets of transitions from s and the refinement relation satisfies for every $(p,q) \in R$:

$$\begin{aligned} \forall M \in \mathrm {Tran}(p) : \exists N \in \mathrm {Tran}(q) :&\quad \forall (a,p') \in M : \exists (a,q') \in N : (p',q') \in R \quad \wedge \\&\quad \forall (a,q') \in N : \exists (a,p') \in M : (p',q') \in R. \end{aligned}$$

For PMTS, intuitively, whatever parameters of the refining system we pick, the abstract system can emulate the same behaviour (by BMTS refinement) for some choice of its parameters. The original definition [BKL+11] requires a single refinement relation for all parameter choices. Later it was superseded by a more natural definition [BKL+15] where different relations are allowed for different parameter valuations; it is closer to the semantically defined notion of thorough refinement, see Definition 10, and keeps the same complexity.

Example 9

Consider the rightmost PMTS in Fig. 9. It has two parameters $reqYfromG$ and $reqYfromR$ whose values can be set independently and it can be refined by the system in the middle of the figure having only one parameter $reqY$. This single parameter binds the two original parameters to the same value. The PMTS in the middle can be further refined into the implementations where either $yellow$ is always used in both cases, or never at all.    $\triangle$

Expressive Power

Most of the formalisms have the same expressive power, as summarized in Fig. 10. However, they differ significantly in succinctness. In [KS13b], PMTS are transformed into exponentially larger BMTS and BMTS into exponentially larger DMTSm, see Fig. 10. Here Cm denotes a class C where systems are considered with more (but only finitely many) initial processes.

Except for the already discussed extra power of MixTS over MTS, mixed variants of systems can be transformed into pure, again at an exponential cost [BK10], up to the inconsistent specification, i.e. specifications with no implementations. Since this difference is not very important, we shall only deal with pure systems unless stated otherwise.

Each of the formalisms presented so far in this section was an automata-based behavioural formalism. These are often preferred as they are easier to read than, for instance, formulae of modal logics. The choice between logical and behavioural specifications is not only a question of preference. Automata-based specifications [Lar89, BG99] have a focus on compositional and incremental design in which logical specifications are somewhat lacking, with the trade-off of generally being less expressive than logics. Logical specification formalisms put a powerful logical language at the disposal of the user, and the logical approach to model checking [QS82, CE81] has seen a lot of success and tool implementations. Therefore, one would like to establish connections between behavioural and logical formalisms to exploit advantages of both at once. The relationship of MTS to logic was studied in [BL92, FP07]. It is established that MTS are equivalent to a fragment of $\mu$-calculus where formulae are (1) consistent, (2) “prime”, meaning the disjunction is allowed only in very special cases, and (3) do not contain the least fixpoint. Further, [BDF+13] proves that DMTSm (and thus BMTS and PMTS) are equivalent to $\nu$-calculus (or Hennessy-Milner logic with greatest fixpoints, abbreviated $\nu$HML), which is a fragment of $\mu$-calculus without the least fixpoint $\mu$. Finally, the refinement corresponds to implication [FLT14], similarly to the refinement calculus for HML with recursion of [Hol89]. Moreover, both formalisms can be equipped with the desired operations coming from the other formalism, see Fig. 11, as further discussed in Sect. 5, bridging the gap between the two approaches.

Fig. 11.

Correspondences between the logical and the behavioural world

Example 10

Consider the following property: “at all time points after executing $\mathsf {request}$, no $\mathsf {idle}$ nor further $\mathsf {request}$s but only $\mathsf {work}$ is allowed until $\mathsf {grant}$ is executed”. The property can be written in e.g. CTL [CE81] as

$$\begin{aligned} \text {AG}(\mathsf {request}\Rightarrow \text {AX}(\mathsf {work}\text { AW } \mathsf {grant})) \end{aligned}$$

Figure 12 shows an example of an equivalent $\nu$HML formula and a DMTS corresponding to this property.    $\triangle$

Fig. 12.

Example of a $\nu$HML formula and an equivalent DMTS

Apart from the logical characterization, one can also describe processes using a process algebra and obtain the discussed subclasses mixed DMTS, pure DMTS, MixTS, MTS, LTS as syntactic subclasses [BK10].

4 Extensions of Transition Systems

The extensions discussed in the previous section focus on what combinations of transitions are possible. In this section, we discuss mainly extensions concerned with quantitative features or infinite memory/communication. Besides, to provide a better basis for interface theories, MTS have been also combined with I/O automata [GSSL94] and interface automata [dAH01] into modal I/O transition systems [LNW07a, RBB+09a, BHJ10, BMSH10, BHW10, BHB10, KM12, KDMU14] with input, output and internal actions, and its subset modal interface automata [LV13, LVF15, BFLV16, SH15]. Other MTS extensions feature specifically modified semantics, e.g., [BV15, BSV15, DSMB16].

4.1 Quantities

Here we discuss lifting the underlying transition systems to quantitative settings [LL12], with clear applications in the embedded systems design. This includes probabilistic specifications (see below) and various weighted specifications, where weights stand for various quantitative aspects (e.g. time, power or memory), which are highly relevant in the area of embedded systems. As far as the particular case of timed systems is concerned, the quantity of time can be refined in various ways. In the early work [CGL93, LSW95], the precise quantities are almost disregarded. More recently [JLS12, BPR09, BLPR09, DLL+10], the possible times are usually specified as time intervals, which can be narrowed down and thus made more specific. A more general option is to permit label refinement to anything smaller with respect to some abstract ordering of labels; [BJL+12a] provides the following conservative extension of MTS modal refinement along these lines:

Definition 7

(Modal refinement of MTS with structured labels). Let the alphabet $\varSigma$ be equipped with an ordering $\sqsubseteq$. Let $(P_1,\mathord {\mathop {\dashrightarrow }\limits ^{}}_1,\mathord {\mathop {\longrightarrow }\limits ^{}}_1),(P_2,\mathord {\mathop {\dashrightarrow }\limits ^{}}_2,\mathord {\mathop {\longrightarrow }\limits ^{}}_2)$ be MTS over $\varSigma$ and $s\in P_1, t\in P_2$ be processes. We say that s modally refines t, written $s\le _mt$, if there is a refinement relation $\mathcal R\subseteq P_1\times P_2$ such that $(s,t)\in \mathcal R$ and for every $(p,q)\in R$ and every $a \in \varSigma$:

• 1. if $p\mathop {\dashrightarrow }\limits ^{a}_{1}p'$ then $q\mathop {\dashrightarrow }\limits ^{{\bar{a}}}_{2}q'$ for some $a\sqsubseteq {\bar{a}}$ and $(p',q')\in R$, and

• 2. if $q\mathop {\longrightarrow }\limits ^{{\bar{a}}}_{2}q'$ then $p\mathop {\longrightarrow }\limits ^{a}_{1}p'$ for some $a\sqsubseteq {\bar{a}}$ and $(p',q')\in R$.

Example 11

Consider $\varSigma =L\times \mathfrak I$ where L is a finite set ordered by identity and $\mathfrak I$ is the set of intervals ordered by inclusion and $\varSigma$ is ordered point-wise, standing for the action and the time required to perform it. A transition labelled by $(\ell ,[a,b])$ can thus be implemented by a transition $(\ell ,c)$ for any $c\in [a,b]$.    $\triangle$

This definition generalizes also previously studied MTS with more weights at once [BJL+12b]. Moreover, one can also consider MTS with timed-automata clocks [BLPR12, FL12]. In all the quantitative settings, it is also natural to extend the qualitative notion of refinement into a quantitative notion of distance of systems [BFJ+11, BFLT12].

Another previously studied instantiation is the modal transition systems with durations (MTSD) [BKL+12]. It models time durations of transitions as controllable or uncontrollable intervals. Controllable intervals can be further refined into narrower intervals, whereas uncontrollable are considered under the control of an unpredictable environment and cannot be further narrowed down. Additionally, the actions are assigned running cost (or rewards) per time unit.

MTS have also been lifted to the probabilistic setting. In the classical setting, LTS is underspecified in that the presence of a certain transition is not specified. For Markov chains, one can underspecify the probability distributions on the outgoing transitions. Interval Markov chains [JL91] describe them with intervals of possible values. Additionally, we can consider 3-valued valuations of atomic propositions in processes (similarly to [HJS01, BG00, CDEG03], useful for abstractions), yielding abstract Markov chains [FLW06]. This approach is extensible also to continuous-time Markov chains [KKLW07, KKLW12]. Besides, constraint Markov chains [CDL+10] use richer constraints than intervals and usual operations on them have also been studied [DLL14]. Finally, abstract probabilistic automata [DKL+11a] combine this with the MTS may-must modality on transitions, allowing for abstractions of Markov decision processes. They have been studied with respect to the supported operations [DKL+11b, DFLL14], state space reduction [SK14], hidden actions (stutter steps) [DLL14], and there is a support by the tool APAC [DLL+11].

Moreover, probabilistic and timed-automata extensions are combined in abstract probabilistic timed automata [HKKG13]. Finally, modal continuous-time automata [HKK13] extend MTS with continuous time constraints on stochastic waiting times, allowing for specification of systems with stochastic continuous time.

Specification theories have been lifted to the quantitative settings and equipped with the notion of distance between systems [BFLT12, FL14, FKLT14, FLT14].

4.2 Infinite State Space

In this section, we consider infinite-state extensions of MTS. Several extensions have been proposed, such as systems with asynchronous communication based on FIFO [BHJ10] or Petri nets [EBHH10, HHM13]. Other extensions focus on input/output extensions of MTS with data constraints [BHB10, BHW10] or explicit representation of data [BLL+14].

A systematic exploration of infinite-state MTS is also possible. A convenient unifying framework for (non-modal) infinite-state systems is provided by process rewrite systems (PRS) [May00]. A PRS $\varDelta$ is a finite set of rewriting rules, which model sequential and parallel computation. Depending on the syntactic restrictions imposed on the rules, we obtain many standard models such as pushdown automata (PDA) or Petri nets (PN), see Fig. 13. A finite PRS $\varDelta$ thus induces possibly infinite LTS $\mathcal {LTS}(\varDelta )$.

Fig. 13.

PRS hierarchy

Example 12

A transition t of a Petri net with input places p, q and output places r, s can be described by the rule $p\parallel q\mathop {\longrightarrow }\limits ^{t} r\parallel s$. A transition of a pushdown automaton in a state s with a top stack symbol X reading a letter a resulting in changing the state to r and pushing Y onto the stack can be written as $s X\mathop {\longrightarrow }\limits ^{a}r YX$.

One can naturally lift PRS to the modal world [BK12] by having two sets of rules: may and must rules. The finite set of rules then generates a generally infinite MTS.

Definition 8

(Modal process rewrite system). A modal process rewrite system (mPRS) is a tuple $\varDelta =(\varDelta _{\mathrm {may}},\varDelta _{\mathrm {must}})$ where $\varDelta _{\mathrm {must}}\subseteq \varDelta _{\mathrm {may}}$ are two PRS. The mPRS $\varDelta$ induces an MTS $\mathcal {MTS}(\varDelta )=(\mathcal E,\mathord {\mathop {\dashrightarrow }\limits ^{}},\mathord {\mathop {\longrightarrow }\limits ^{}})$ defined by $(\mathcal E,\mathord {\mathop {\dashrightarrow }\limits ^{}})=\mathcal {LTS}(\varDelta _{\mathrm {may}})$ and $(\mathcal E,\mathord {\mathop {\longrightarrow }\limits ^{}})=\mathcal {LTS}(\varDelta _{\mathrm {must}})$.

Each subclass $\mathcal C$ of PRS has a corresponding modal extension $\mathrm m\mathcal C$ containing all mPRS $(\varDelta _{\mathrm {may}},\varDelta _{\mathrm {must}})$ with both $\varDelta _{\mathrm {may}}$ and $\varDelta _{\mathrm {must}}$ in $\mathcal C$. For instance, mFSM correspond to the standard finite MTS and mPN are modal Petri nets as introduced in [EBHH10].

Definition 9

(Modal refinement). Given mPRS $\varDelta _1\in m\mathcal C_1,\varDelta _2\in m\mathcal C_2$ and process terms $\delta _1,\delta _2$, we say $\delta _1$ refines $\delta _2$, written $\delta _1\le _m\delta _2$, if $\delta _1\le _m\delta _2$ as processes of $MTS(\varDelta _1)$ and $MTS(\varDelta _2)$, respectively.

What is the use of infinite MTS? Firstly, potentially infinite-state systems such as Petri nets are very popular for modelling whenever communication and/or synchronization between processes occurs. This is true even in cases where they are actually bounded and thus with a finite state space.

Example 13

Consider the following may rule (we use dashed arrows to denote may rules) generating a small Petri net.

$$\begin{aligned}\mathsf {resource\mathop {\dashrightarrow }\limits ^{produce}money\parallel trash}\end{aligned}$$

If this is the only rule with $\mathsf {trash}$ on the right side a safety property is guaranteed for all implementations of this system, namely that $\mathsf {trash}$ can only arise if there is at least one $\mathsf {resource}$. On the other hand, it is not guaranteed that $\mathsf {money}$ can indeed be produced in such a situation. This is very useful as during the design process new requirements can arise, such as necessity of adding more participants to perform this transition. For instance,

expresses an auxiliary condition required to produce $\mathsf {trash}$, namely that a $\mathsf {permit}$ is available. Replacing the old rule with the new one is equivalent to adding an input place $\mathsf {permit}$ to the modal Petri net, see Fig. 14 in yellow. In the modal transition system view, the new system refines the old one. Indeed, the new system is only more specific about the allowed behaviour than the old one and does not permit any previously forbidden behaviour.

Fig. 14.

A modal Petri net given by rules $\mathsf {Resource} {\parallel \mathsf {Permit}} \mathop {\dashrightarrow }\limits ^{\mathsf {produce}} \mathsf {Money} \parallel \mathsf {Trash}$ and $\mathsf {Trash} \mathop {\longrightarrow }\limits ^{\mathsf {clean}} \mathsf {Permit}$ with may transitions drawn as empty boxes and must transitions as full boxes (Color figure online)

One can further refine the system into the one given by

$$\begin{aligned} \mathsf {resource \parallel permit\parallel bribe\mathop {\longrightarrow }\limits ^{produce}money\parallel trash} \end{aligned}$$

where additional condition is imposed and now the $\mathsf {money}$-producing transition has to be available (denoted by an unbroken arrow) whenever the left hand side condition is satisfied.    $\triangle$

Further, infinitely many states are useful to capture unbounded memory. For instance, consider a specification where the total amount of $\mathsf {permit}$s is not explicitly limited. In an implementation, the number of $\mathsf {permit}$s might need to be remembered in the state of the system.

Example 14

Consider a basic process algebra (BPA) given by rules $X\mathop {\longrightarrow }\limits ^{(}X X$ and $X\mathop {\longrightarrow }\limits ^{)}\varepsilon$ for correctly parenthesized expressions with $X\mathop {\dashrightarrow }\limits ^{a}X$ for all other symbols a, i.e. with no restriction on the syntax of expressions. One can easily refine this system into a PDA that accepts correct arithmetic expressions by remembering in a control state whether the last symbol read was an operand or an operator.    $\triangle$

5 Analysis

In this section, we survey algorithms for and complexities of the most important problems on MTS and their extensions.

5.1 Refinements

Modal refinement is a syntactically defined notion extending both bisimulation and simulation. Similarly to bisimulation having a semantic counterpart in trace equivalence, here the semantic counterpart of modal refinement is the thorough refinement. As opposed to the syntactic definition using local notions, the semantic definition relates (by inclusion) the sets of implementations of the specifications. The definition is universal for all extensions of MTS as it only depends on the notion of implementation and not on syntax of the particular extension.

Definition 10

(Thorough refinement). Given processes s and t, we say that s thoroughly refines t, written $s\le _tt$, if $\llbracket {s}\rrbracket \subseteq \llbracket {t}\rrbracket$.

Note that the two refinements are in general different as we illustrate in the following example due to [BKLS09b], simplifying [HL89]:

Example 15

Consider processes s and t of Fig. 15. On the one hand, the sets of implementations of s and t are the same, namely those that can perform either no action or one a or two a’s or combine the latter two options. On the other hand, s does not modally refine t. Indeed, whenever $s\le _mt$ then either $s'\le _mt_1$ or $s'\le _mt_2$. However, neither is true, as $s'$ allows a transition while $t_1$ does not, and $s'$ does not require any transition while $t_2$ does.

Although the two refinements differ, modal refinement is a sound under-approximation of the thorough refinement. Indeed, whenever we have $s\le _mt$ and $i\in \llbracket {s}\rrbracket$ we also have $i\le _ms$ and by transitivity of the modal refinement we obtain $i\le _mt$.

Proposition 1

Let s, t be processes. If $s\le _mt$ then $s\le _tt$.

Moreover, [BKLS09b] shows the other direction holds whenever the refined system is deterministic. A process is deterministic if, for each process s of its underlying MTS and for each $a \in \varSigma$, there is at most one $s'$ such that $s \mathop {\dashrightarrow }\limits ^{a} s'$.

Fig. 15.

$s \le _tt$, but $s \not \le _mt$

Proposition 2

Let s, t be processes and t deterministic. If $s\le _tt$ then $s\le _mt$.

In Table 1 we give an overview of the results related to deciding modal and thorough refinements for different combinations of processes on the left- and right-hand side (here D stands for deterministic processes and N for non-deterministic processes). Note that the co-inductive refinement relations are easy to compute using a fixed-point computation, although other methods are also possible, e.g. logical programming [AKRU11] or QBF solving [KS13b, BKL+15].

Table 1. MTS refinement complexity for various cases of (non)determinism

Since the thorough refinement is EXP-hard, it is much harder than the modal refinement. Therefore, we also investigate how the thorough refinement can be approximated by the modal refinement. While under-approximation is easy, as modal refinement implies thorough refinement, over-approximation is more difficult. Here one can use the method of the deterministic hull for MTS [BKLS09b]. The deterministic hull $\mathcal {D}$ is a generalization of the powerset construction on finite automata and it is the smallest (w.r.t. modal refinement) deterministic system refined by the original system.

Proposition 3

Let s be an arbitrary MTS process. Then $\mathcal {D}(s)$ is a deterministic MTS process such that $s\le _m\mathcal {D}(s)$ and, for every deterministic MTS process t, if $s\le _tt$ then $\mathcal {D}(s)\le _mt$.

Corollary 1

For any processes s, t, if $s\not \le _m\mathcal {D}(t)$ then $s \not \le _tt$.

There are also other notions of refinements of systems close to MTS, such as alternating refinements [AHKV98, AFdFE+11], branching refinement [FBU09], refinement preserving the termination possibility [CR12], or refinement for product lines [DSMB16].

Extensions. As to extensions of MTS with more complex modalities, the local conditions in modal refinement are more complex. Although various extensions have the same expressive power (see Fig. 10), the transformations are exponential and thus the extensions differ in succinctness. Therefore, the respective refinement problems are harder for the more succinct extensions. All the cases depending on the type of the left-hand and right-hand sides are discussed in [BKL+15]. In most cases without parameters, the refinement can be decided in P or NP, which is feasible using SAT solvers. For systems with parameters, the complexity is significantly higher, reaching up to $\mathrm \Pi ^\mathrm p_4$. Since all the complexities are included in PSPACE, QBF solvers have been applied to this problem, improving scalability to systems with hundreds of states [KS13c, BKL+15]. The QBF approach basically eliminates the complexity threat of parameters, but is quite sensitive to the level of non-determinism.

Furthermore, the decision algorithm for thorough refinement checking over MTS [BKLS12, BKLS12] has been extended to the setting of DMTS [BČK10] and of BMTS and PMTS [KS13b], see Table 2. [KS13b] also generalizes the notion of the deterministic hull.

Table 2. Complexity of the thorough refinement and the relationship to the modal refinement

We now turn our attention to the refinement problems on other kinds of extensions of MTS. Assuming polynomial procedures for operations on structured labels, the complexity of the modal refinement stays the same as for the underlying MTS. As for infinite state systems, [BK12] shows that refinement between finite MTS and modal pushdown automaton and between modal visibly pushdown automata is decidable and EXP-complete, whereas between basic process algebras it is undecidable. When parallelism is involved, undecidability occurs very soon, already for finite MTS and basic parallel process. However, it is decidable for Petri nets when a weak form of determinism is imposed [EHH12, HHM13]. Finally, in the spirit of [AHKV98], a symmetric version of refinement resulting into a bisimulation notion over MTS is considered and shown decidable between a finite MTS and any modal process rewrite system, using the results of [KŘS05]. This allows us to check whether we can replace an infinite MTS with a particular finite one, which in turn may allow for checking further refinements.

5.2 Operations

Specification theories require the specification formalism to be closed under certain operations, as described in Sect. 2. However, not all classes of modal systems support all the operations. As an automata-based formalism, MTS automatically allow to compose systems structurally, whereas logical operations are either difficult to compute or cannot be expressed in the formalism at all. Therefore, most of the focus has been directed to the simple deterministic case, where some operations can be defined using local syntactic rules, even for the quantitative extensions [BFJ+13].

Fig. 16.

MTS processes $s_1, s_2$, their greatest lower bound $(s_1,s_2)$, and their two maximal MTS lower bounds $M_1, M_2$

• $\parallel$ The parallel composition can often be lifted to the modal setting simply by applying the same SOS rules, e.g. for synchronous message passing, to both may and must transition functions. This holds for a wide class of operators as described in [BKLS09b] for MTS. Parallel composition can be extended to DMTS and other classes [BČK10, BDF+13]. Unfortunately, they inherit the incompleteness with respect to modal refinement from MTS, see [HL89, BKLS09b]. Therefore, the axiom (parallel) is only satisfied in one direction (the independent implementability), but not every implementation of the composition can actually be decomposed into a pair of implementations, see Fig. 5, and in general we have $\llbracket {s}\rrbracket \parallel \llbracket {t}\rrbracket \subset \llbracket {s\parallel t}\rrbracket$.

• $/$ The quotient for deterministic MTS can be defined syntactically, using a few SOS rules [Rac07, Rac08]. For non-deterministic MTS, the problem is considerably more complex and the question was open for a long time. A construction for BMTS and DMTSm and an exponentially smaller one for MTS was given in [BDF+13]. Further related questions such as decomposition of a system into several components put in parallel [SUBK12] or quotient under reachability constraints [VR15] have also been investigated, but again only for deterministic systems.

• $\wedge$ The situation is similar with conjunction. For deterministic MTS, we can again define it syntactically. For non-deterministic systems, there were several attempts. Unfortunately, the resulting MTS is not minimal (with respect to modal refinement) [UC04], or not finite even when claimed to be finite [FU08]: the “clone” operation may not terminate even in cases when it is supposed to, for example, for processes $s_1,s_2$ of Fig. 16 where the self-loops are redirected back to the initial processes. Actually, MTS are not closed under conjunction, see Fig. 16. However, a conjunction of two MTS has a unique greatest DMTS solution.

  Moreover, DMTS with one or more initial processes, and thus also BMTS and PMTS are closed under conjunction [BČK11]. The result of the construction is based on the synchronous product. Thus it is a system over tuples of processes where the length of the tuple is the number of input systems. This means that the conjunction (and thus also a common implementation) can be constructed in polynomial time, if n is fixed; and in exponential time, if n is a part of the input. Further, if deterministic MTS are input, the algorithm produces a deterministic MTS. Moreover, the conjunction is also the greatest lower bound with respect to the thorough refinement: $\llbracket { s_1\wedge s_2}\rrbracket = \llbracket { s_1}\rrbracket \cap \llbracket { s_2}\rrbracket$ which is not achievable for the parallel composition. The conjunction construction was later extended to systems with different alphabets [BDCU13] and invisible actions [BCU16].

• $\vee$ Disjunction is easy to obtain for DMTSm, BMTS, and PMTS, again in the stronger form $\llbracket { s_1\vee s_2}\rrbracket =\llbracket { s_1}\rrbracket \cup \llbracket { s_2}\rrbracket$. However, for MTS (deterministic or not) and DMTS with a single initial process this is not possible. Indeed, consider the MTS specifications in Fig. 17. While the disjunction can be described simply as a BMTS with obligation $\varOmega (s_1\vee s_2)=((a,\bullet )\wedge (b,\bullet )) \vee (\lnot (a,\bullet )\wedge \lnot (b,\bullet ))$, no DMTS can express this.

• $\lnot$ While MTS are not closed under complement (not even deterministic ones), there have been attempts at characterizing symmetric difference [SCU11].

Fig. 17.

MTS $s_1$ and $s_2$, and their MTS and BMTS least upper bounds $s_1\vee s_2$

The results are summed up in the following statements and Table 3. With operations $\wedge$ and $\vee$, the set of BMTS (or DMTSm) processes forms a bounded distributive lattice up to $(\le _m\cap \ge _m)$-equivalence. Moreover, with operations $\wedge , \vee , \Vert$ and $/$, the set of BMTS (or DMTSm) forms a commutative residuated lattice up to $(\le _m\cap \ge _m)$-equivalence [BDF+13].

Table 3. Closure properties

We are also interested in questions closely related to the discussed conjunction. The common implementation decision problem ($\mathrm {CI}$) contains tuples of systems, such that there is an implementation refining each system of the tuple. For tuples of size two this is equivalent to non-emptiness of the conjunction, for one system (for instance a MixTS) this is equivalent to semantic consistency (or non-emptiness) [LNW07b], i.e. existence of implementation. Note that despite the lack of results on conjunction of non-deterministic systems the complexity was known long ago. The complexity improves when the input processes are deterministic ($\mathrm {CI}_{\mathrm D}$ problem). Finally, rather surprisingly, the problem whether there is a deterministic common implementation ($\mathrm {dCI}$) is hard. We display the known results in Table 4 for several cases depending on whether the number of input processes is fixed or a part of the input. The results again indicate that several problems become more tractable if the given specifications are deterministic.

Table 4. Complexity of the common implementation problems

5.3 Model Checking and Synthesis

Given a valuation $\nu :P\rightarrow 2^{Ap}$ assigning to each process a set of atomic propositions valid in the process, one can check whether an MTS satisfies a CTL, LTL or $\mu$-calculus formula $\varphi$ over Ap. Since an MTS stands for a class of implementations, the question of satisfaction can be posed in two flavours:

• ( $\models _\forall$ -problem) Do all implementations satisfy $\varphi$?

• ( $\models _\exists$ -problem) Is there an implementation satisfying $\varphi$?

The problem of generalized model checking is to decide which of the three possible cases holds: whether all, only some, or no implementations satisfy $\varphi$. Further, if there exists a satisfying implementation it should also be automatically synthesized.

Generalized model checking of MTS was investigated with respect to a variant of safety [DDM10] as well as computation tree logic (CTL) [AHL+08a, GAW13], establishing it EXP-complete and providing a polynomial over- and under-approximation, similarly for $\mu$-calculus. The EXP lower bound follows from the hardness of satisfiability of CTL and $\mu$-calculus; the upper bound can be obtained through alternating tree automata [BG00].

In the rest, we focus on LTL. In [GP09] the generalized model checking of LTL over partial Kripke structures (PKS) is shown to be 2-EXP-hard. Further, [GJ03] describes a reduction from generalized model checking of $\mu$-calculus over PKS to $\mu$-calculus over MTS [Hut02, Hut99, GHJ01]. However, the hardness for LTL does not follow since the encoding of an LTL formula into $\mu$-calculus is exponential. There is thus no straightforward way to use the result of [GJ03] to establish the complexity for LTL.

On the one hand, answering the $\models _\forall$-problem is easy. Indeed, it is sufficient to perform standard model checking on the “greatest” implementation, i.e. such where all mays are turned into musts and thus all possible runs are present. On the other hand, the $\models _\exists$-problem is trickier. Similarly to the for $\models _\forall$-problem, we can take the minimal implementation of the MTS. However, whenever a deadlock occurs, the corresponding finite runs are ignored since LTL is usually interpreted over infinite words only. However, an undesirable consequence of this problem definition (call it $\omega$, standing for infinite runs) is that all formulae are satisfied whenever there is an implementation without infinite runs, i.e. without a lasso of must transitions. There are several ways to avoid this vacuous satisfaction. Firstly, we can define LTL also on finite words [BČK11], which we denote by $\infty$ (for both finite and infinite runs). Secondly, we can consider only implementations without deadlocks, which we denote df. The deadlock-free approach has been studied in [UBC09] and the proposed solution was implemented in the tool MTSA [DFCU08]. It attempts to find a deadlock-free implementation of a given MTS that satisfies a given formula. However, the solution given in [UBC09] is incorrect in that the existence of a deadlock-free implementation satisfying a given formula is claimed even in some cases where no such implementation exists.

Example 16

The flaw can be seen on an example given in Fig. 18 [BČK11]. Clearly, s has no deadlock-free implementation with action a only, i.e. satisfying $\mathbf {G}\mathbf {X}_a \mathbf {tt}$. Yet the method of [UBC09] as well as the tool [DFCU08] claim that such an implementation exists.    $\triangle$

Fig. 18.

No deadlock-free implementation of s satisfies $\mathbf {G}\mathbf {X}_a \mathbf {tt}$

While the solution attempt of [UBC09] yields a PSPACE algorithm, the df-problem is actually 2-EXP-complete[BČK11]. Note that in this setting, there are no minimal implementations; non-trivial decisions have to be made which transitions to implement. For example, an MTS with only one may a-successor and one may b-successor cannot avoid deadlock in a unique way. Moreover, even if deadlocks are allowed, not implementing any choice may result in not satisfying $\mathbf {X}\mathbf {tt}$.

A solution to both df and $\infty$ as well as DMTS is provided in [BČK11]. It reduces the problem to a game where one player decides which transitions to implement in each step and another player chooses which of the implemented transitions is taken. Decisions of the players determine a run. The objective of the first player is to satisfy the formula on the run. He can always succeed irrespective of what the other player does if and only if there is an implementation satisfying the formula. Such LTL games are in general 2-EXP-complete [PR89]. The consequences are summarized in Table 5. Note that the winning strategy in the game yields a satisfying implementation, thus also solving the synthesis problem. This approach of reduction to an LTL game was also used to solve a similar problem of deciding whether all/some implementation can be pruned to satisfy a given LTL formula [DBPU12].

Table 5. Complexities of generalized LTL model checking ($\omega$ denoting finite runs are ignored, df denoting deadlock-free implementations are ignored, $\infty$ denoting no restriction)

The best known time complexity bounds with respect to the size of system $|S|$ and the size of LTL formula $|\varphi |$ are the following. In all PSPACE-complete cases the time complexity is $\mathcal O(|S|\cdot 2^{|\varphi |})$; in all 2-EXP-complete cases the time complexity is $|S|^{2^{\mathcal O(|\varphi |)}} \cdot 2^{2^{\mathcal O(|\varphi |)}}$. The latter upper bound is achieved by translating the LTL formula into a deterministic (possibly generalized) Rabin automaton of size $2^{2^{\mathcal O(|\varphi |)}}$ with ${2^{\mathcal O(|\varphi |)}}$ accepting pairs, thus changing the LTL game into a Rabin game. For an efficient translation see e.g. [EK14, KK14]; for an algorithm solving Rabin games see [PP06, CGK13].

Another synthesis problem is the cheapest implementation, considered for (P)MTS with durations [BKL+12]. Intuitively, the constraint on the implementation here is to maximize the average reward per time unit while conforming to the specification and a budget allowing only for some combinations of actions implemented. The problem is NP-complete. Further, the problem of synthesizing a satisfying implementation in the form of a bounded Petri net was considered and shown undecidable [Sch16]. Finally, MTS themselves can be synthesized from constraints given as e.g. scenarios [SBUK13].

LTL model checking has also shed a better light on the problem of incompleteness of the parallel composition. Recall that there is a composition $s_1\parallel s_2$ with an implementation i that does not arise as a composition $i_1\parallel i_2$ of any two implementations $i_1\le _ms_1, i_2\le _ms_2$. Completeness can be achieved only under some restrictive conditions [BKLS09b]. [BČK11] shows that composition is sound and complete with respect to every logic of linear time: For DMTS and both $\omega$ and $\infty$,

$$\begin{aligned} s_1\parallel s_2\models _\forall \varphi&\text { iff } i_1\parallel i_2\models \varphi \text { for all implementations } i_1\le _ms_1, i_2\le _ms_2\\ s_1\parallel s_2\models _\exists \varphi&\text { iff } i_1\parallel i_2\models \varphi \text { for some implementations } i_1\le _ms_1, i_2\le _ms_2 \end{aligned}$$

Thus $\parallel$ is “LTL complete”, i.e. preserves and reflects all LTL properties. Therefore, the only spurious implementations are sums of legal implementations.

6 Tools

The tool support is quite extensive; we focus our attention to the support for the operations required for complete specification theories [BDH+12] and several further problems. This includes modal refinement checking, parallel composition, quotient, conjunction (merge) and the related consistency checking and maximal implementation generation, deterministic hull and generalized LTL model checking. The comparison of the functionality of the available tools is depicted in Table 6. Apart from no longer maintained TAV [BLS95], the currently available tools are the following:

MTSA (Modal Transition System Analyzer) [DFFU07]

• is a tool for MTS,

• supports modal refinement, parallel composition and consistency using the cloning operation, which may not terminate; it also offers a model checking procedure, which is, unfortunately, flawed as discussed in Example 16.

MIO (Modal Input Output Workbench) [BML11, BMSH10]

• is a tool for modal I/O automata (MIOA) [LNW07a, RBB+11], which combine MTS and interface automata based on I/O automata; although MIOA have three types of may and must transitions (input, output, and internal), if we restrict to say only input transitions, the refinement works the same as for MTS, and some other operations, too,

• supports modal refinement, the MIOA parallel composition, conjunction for deterministic systems, and quotient for deterministic systems.

${\mathop {\mathrm {MoTraS}}\limits ^{\mathop {\longrightarrow }\limits ^{}\Longrightarrow \mathop {\dashrightarrow }\limits ^{}}}$ (Modal Transition Systems) [KS13a]

• is a tool for MTS and DMTS, with partial support for BMTS and PMTS,

• supports full functionality for MTS as well as more general DMTS and in all cases also for non-deterministic systems; in particular, the algorithms for conjunction and quotient are considerably more complex than for the deterministic case; further, it features QBF-based algorithms for BMTS and PMTS refinement; finally, it also provides the deterministic hull, which enables us to both over- and under-approximate the very hard thorough refinement using the fast modal refinement.

MAccS (Marked Acceptance Specifications) [VR14]

• is a tool for acceptance automata (deterministic BMTS) with accepting states,

• features all the operations for acceptance automata, hence also for deterministic MTS.

Note that both MTSA and MIO can only handle modal systems, not their disjunctive extension. MoTraS supports DMTS, which have more expressive power. In contrast to (non-deterministic) MTS, DMTS are rich enough to express solutions to process equations [LX90] (hence a specification of a missing component in a system can be computed) and are closed under all operations, particularly conjunction. MAccS is similar in that AA are equally expressive and it supports all the operations, however, only for deterministic systems.

In order to make the tools easily extensible, a file format xmts was designed [MTS], which facilitates textual representation of different extensions of modal transition systems.

Table 6. Functionality of the available tools. Here “det.” denotes a functionality limited to deterministic systems.

Besides, there are the following tools for related formalisms:

ECDAR (Environment for Compositional Design and Analysis of Real Time Systems) [DLL+10]

• is a tool for timed I/O automata (with no modalities);

• supports refinement, conjunction, composition and quotient, but all for only deterministic systems, as can be expected in the timed setting.

APAC (Abstract Probabilistic Automata Checker) [DLL+11]

• is a tool for abstract probabilistic automata;

• supports refinement, abstraction, conjunction, and composition.

7 Conclusion and Some Directions for Future Work

Firstly, we have surveyed MTS and its many extensions, including more involved modalities (combined, exclusive, persistent or conditional choices), quantitative models, or infinite-state systems. The comparison of various classes leads us to identifying a robust class of DMTS with more initial states, equivalent to several other formalisms, including the modal $\nu$-calculus. This unifies the behavioural and logical approach to specification and verification and enables us to mix the two.

Secondly, we have surveyed solutions to problems arising in system design via MTS, such as logical and structural operations, refinement (modal, thorough, approximations using the deterministic hull) and synthesis of implementations based on temporal or reward constraints. We have also discussed the tool support for these problems.

As for future work, we mention several open issues. Firstly, although the complexity of many problems has been established, there are still several complexity gaps left open, for instance, the complexity of thorough refinement for BMTS and PMTS, the quotient construction (we conjecture the exponential blow-up is in general unavoidable), whether MTS, MixTS and DMTS are closed under quotient (we conjecture the opposite), or conditions on decidability of refinement over infinite systems, e.g. determinism as in [BKLS09b, EBHH10, HHM13].

Secondly, one may also extend the model checking and synthesis algorithms to more complex settings such as the cheapest implementation with an additional requirement that the partial sums stay within given bounds as done in [BFL+08], or cheapest implementation satisfying a temporal property as suggested in [CdAHS03, CD10], model checking metric temporal logic (LTL with time durations) [Koy90], model checking infinite-state MTS similarly to PDA in [Wal96], or cheapest implementation of mPDA using methods like [CV12].

Thirdly, on the practical side, all the tools only offer a limited support. In particular, the quotient of non-deterministic systems is very important for practical design and has not yet been implemented. Refinement algorithms do not scale too well on MTS extensions. Apart from multi-threading for all algorithms, one could use a combined modal refinement checker, which uses the standard modal refinement checker to prune the initial relation before the QBF-based checker is called. Altogether, the topic is still lively and subject to further practical developments, e.g. the currently prepared update of ${\mathop {\mathrm {MoTraS}}\limits ^{\mathop {\longrightarrow }\limits ^{}\Longrightarrow \mathop {\dashrightarrow }\limits ^{}}}$ features faster model checking due to integrating a better LTL-to-automata translator Rabinizer 3 [KK14] and the cheapest implementation synthesizer [BKL+12, Man13].

Finally, the practical usability of MTS could be greatly improved by providing a higher-level language, possibly tailored to particular domains, which has MTS semantics, but a friendlier appearance to the domain-specific engineering practice.