Specification decomposition is a theoretically interesting and practically relevant problem for which two approaches were independently developed by the control theory and verification communities: natural projection and partial model checking. In this paper we show that, under reasonable assumptions, natural projection reduces to partial model checking and, when cast in a common setting, the two are equivalent. Aside from their theoretical interest, our results build a bridge whereby the control theory community can reuse algorithms and results developed by the verification community. In addition, we present an algorithm and a tool for the partial model checking of finite-state automata that can be used as an alternative to natural projection.
Hinweise
G. Costa and L. Galletta—The current address of the authors is IMT Lucca.
1 Introduction
System verification requires comparing a system’s behavior against a specification. When the system consists of several components, we can distinguish between local and global specifications. A local specification applies to a single component, whereas a global specification should hold for the entire system. Since these specifications are needed to reason at different levels of abstraction, both of them are often present.
Ideally, we would like to freely pass from local to global specifications and vice versa. Most specification formalisms natively support specification composition. Logical conjunction, set intersection, and the synchronous product of automata are all examples of operators for composing specifications. Unfortunately, the same does not hold for specification decomposition: obtaining local specifications from a global one is, in general, extremely complex, as illustrated below.
Anzeige
Example 1
Consider the classical submodule construction problem (SCP) [27]: given a system and a global specification, find a submodule whose composition with the system leads to a global behavior conformant to the global specification. For instance, imagine that we aim to control the usage of a buffer of size n, where two agents, A and B, can insert and remove items. Now assume that A’s behavior is to “insert one item when the buffer is empty and delete one item when it is full”, while B’s behavior is unknown. If we want to prevent buffer overflow and underflow, some questions arise about B. For example, are there compatible behaviors for B? Is there a most general one? How could we effectively compute it? These questions require decomposing the buffer overflow/underflow specification so that it only refers to B, while exploiting the known structure of A. \(\square \)
Over the past decades, researchers have investigated methods for decomposing specifications. Interestingly, different communities have tackled this problem independently, each considering specification formalisms and assumptions appropriate for their application context. In particular, important results were obtained in two distinct fields: control theory and formal verification.
In control theory, natural projection [33] is used for simplifying systems built from multiple components, modeled as automata. It is often applied component-wise to synthesize local controllers from a global specification of asynchronous discrete-event system [9], namely the controller synthesis problem (CSP). Briefly, local controllers guarantee that the global specification is not violated by interacting only with a single component of a system. The local controllers can be used to implement distributed control systems [34, 35] by composing them in parallel with other sub-systems.
Table 1.
Summary of existing results on natural projection and partial model checking. Notice that the algorithm in [32] runs in PTIME on a specific class of discrete-event systems.
In the formal verification community, partial model checking [1] was proposed as a technique for mitigating the state explosion problem when verifying large systems built from many parallel processes. Partial model checking tackles this problem by decomposing a specification, given as a formula of the \(\mu \)-calculus [22], using a quotienting operator, thereby supporting the analysis of the individual processes independently. Quotienting carries out a partial evaluation of a specification while preserving the model checking problem. Thus, a system built by composing two modules satisfies a specification if and only if one of the modules satisfies the specification after quotienting against the other [1]. This may reduce the problem size, resulting in smaller models and hence faster verification.
Anzeige
Table 1 summarizes some relevant facts about the two approaches and we refer the reader to Sect. 5 for a more detailed analysis. Since natural projection and partial model checking apply to different formalisms, they cannot be directly compared without defining a common framework (see below). For instance, a relevant question is comparing how specifications grow under the two approaches. Although it is known that both may lead to exponential growth (see [3, 21, 32]), these results apply in one case to finite-state automata (FSAs) and in the other case to \(\mu \)-calculus formulae.
Over the past few years, there has been a substantial cross-fertilization between the two research communities [12]. For instance, methods for synthesizing controllers using partial model checking are given in [6, 25]. The authors of [15, 17] propose similar techniques, but they use fragments of the \(\mu \)-calculus and CTL\(^*\), respectively.
We follow here the suggestion of Ehlers et al. [12], who advocate formally connecting these two approaches so as to make them interchangeable. In their words:
“Such a formal bridge should be a source of inspiration for new lines of investigation that will leverage the power of the synthesis techniques that have been developed in these two areas. [...] It would be worthwhile to develop case studies that would allow a detailed comparison of these two frameworks in terms of plant and specification modeling, computational complexity of synthesis, and implementation of derived supervisor/controller.”
As for the first remark, we show that, under reasonable assumptions, natural projection reduces to partial model checking and, when cast in a common setting, they are equivalent. To this end, we first define a common theoretical framework for both. In particular, we slightly extend both the notion of natural projection and the semantics of the \(\mu \)-calculus in terms of the satisfying traces. These extensions allow us to apply natural projection to the language denoted by a specification. In addition, we extend the main property of the quotienting operator by showing that it corresponds to the natural projection of the language denoted by the specification, and vice versa (Theorem 4).
We provide additional results that contribute to the detailed comparison referred to in the second remark. Namely we define a new algorithm for partial model checking directly on LTSs (rather than on the \(\mu \)-calculus). We prove our algorithm correct with respect to the traditional quotienting rules and we show it runs in polynomial time, like the algorithms based on natural projection. We have implemented this algorithm in a tool, which is available online [11]. Along with the tool, we developed several case studies illustrating its application to the synthesis of both submodules and local controllers.
Structure of the paper. Section 2 presents our unified theoretical framework for natural projection and partial model checking. Section 3 contains our main theoretical results, in particular Theorem 4 on the equivalence of quotienting and natural projection. In Sect. 4 we introduce a novel quotienting algorithm, discuss its properties, and apply it to our running example. In Sect. 5 we briefly survey the related literature and in Sect. 6 we draw conclusions. The formal proofs together with the correctness and the complexity of our algorithm, and our experimental results are available at https://github.com/SCPTeam/pests/blob/master/proofs_and_experiments.pdf.
2 A General Framework
In this section we cast both natural projection and partial model checking in a common framework. We start with a running example: a scenario inspired by [10, 33], which is an instance of Example 1.
Example 2 (Running example)
A drone package delivery (DPD) system relies on unmanned aerial vehicles (UAVs) to transport goods within a given area. Drones interact with docking stations where they can pick up (action u) or deposit (action d) an item. These actions are only observable to the docking station. Additional interactions are represented by the two control actions s (for synchronize) and t (for terminate). An action t takes place when UAVs are requested to leave the station, e.g., due to a maintenance operation, while s is used for the global synchronization of both the docking station and UAVs.
Figure 1 depicts a transition system that encodes the specification of an n-position buffer P(n) handled by a docking station. Intuitively, UAVs cannot perform d actions when the buffer is full (state \(p_n\)) and u actions when the buffer is empty (state \(p_0\)). Since synchronization actions s and t are immaterial, they label self-loops. \(\square \)
Fig. 1.
An n-positions buffer specification P(n).
×
2.1 Language Semantics Versus State Semantics
Natural projection is commonly defined over (sets of) words [33]. Words are finite sequences of actions, i.e., symbols labeling each transition between two states of a finite-state automaton (FSA). The language of an FSA is the set of all words that label a sequence of transitions from an initial state to some distinguished state, like a final or marking state. We call the function \(\mathcal {L}\) that maps each FSA to the corresponding language semantics. Given a system T and a specification S, both FSAs, then T is said to satisfy S whenever \(\mathcal {L}(T) \subseteq \mathcal {L}(S)\).
For partial model checking, the specification S is defined by a formula of the \(\mu \)-calculus. In this case, the standard interpretation is given by a state semantics, i.e., a function that given a system T and a formula \(\varPhi \) returns the set of states of T that satisfy \(\varPhi \). Usually, T is given as a labeled transition system (LTS). An LTS is similar to an FSA, but with a weaker notion of acceptance, where all states are final. A set of evaluation rules formalizes whether a state satisfies a formula or not. Given an LTS T and a \(\mu \)-calculus formula \(\varPhi \), we say that T satisfies \(\varPhi \) whenever its initial state does.
The language semantics of temporal logics is strictly less expressive than the state-based one [16]. A similar fact holds for FSA and regular expressions [5]. Here we use a semantics from which both the state-based and the language semantics can be obtained.
2.2 Operational Model and Natural Projection
We now generalize slightly the existing approaches based on partial model checking and on supervisory control theory used for locally verifying global properties of discrete event systems. We then constructively prove that the two approaches are equally expressive so that techniques from one can be transferred to the other. To this end, we consider models expressed as (finite) labeled transition systems, which describe the behavior of discrete systems. In particular, we restrict ourselves here to deterministic transition systems.
Definition 1
A (deterministic) labeled transition system (LTS) is a tuple \(A = (S_A, \varSigma _A, \rightarrow _A, \imath _A)\) where \(S_A\) is a finite set of states (with \(\imath _A\) the initial state), \(\varSigma _A\) is a finite set of action labels, and \(\rightarrow _A : S_A \times \varSigma _A \rightarrow S_A\) is the transition function. We write \(t = s \xrightarrow {a} s'\) to denote a transition, whenever \(\rightarrow _A(a,s) = s'\), and we call s the source state, a the action label, and \(s'\) the destination state.
A trace\(\sigma \in {\mathcal T}\) of an LTS A is either a single state s or a sequence of transitions \(t_1 \cdot t_2 \cdot \dots \) such that for each \(t_i\), its destination is the source of \(t_{i+1}\) (if any). When unnecessary, we omit the source of \(t_{i+1}\), and write a trace as the sequence \(\sigma = s_0 \mathbf{a_1} s_1 \mathbf{a_2} s_2 \ldots \mathbf{a_n} s_n\), alternating elements of \(S_A\) and \(\varSigma _A\) (written in boldface for readability). Finally, we denote by \([\![{A,s}]\!]_{}^{}\) the set of traces of A starting from state s and we write \([\![{A}]\!]_{}^{}\) for \([\![{A,\imath _A}]\!]_{}^{}\), i.e., for those traces starting from the initial state \(\imath _A\). \(\square \)
Example 3
Consider again our running example. Figure 2 depicts the LTSs A and B. A models an UAV that deposits (d) two items in the buffer and performs a synchronization action (s). Optionally, A can also leave the docking station (t). In contrast, B repeatedly picks an item and synchronizes. Both A and B may also leave the docking station (t). Notice that the traces \([\![{A}]\!]_{}^{}\) starting from the initial state of A are \([\![{A}]\!]_{}^{} = \{q_0, q_0 \mathbf{d} q_1, q_0 \mathbf{t} q_3, q_0 \mathbf{d} q_1 \mathbf{d} q_2, q_0 \mathbf{d} q_1 \mathbf{d} q_2 \mathbf{s} q_0, \ldots \}\). In contrast, the traces starting from the initial state of B are
Typically, a system, or plant in control theory terms, consists of multiple interacting components running in parallel. Below we rephrase the synchronous product of [33]. Intuitively, when two LTSs are put in parallel, each proceeds asynchronously, except on those actions they share, upon which they synchronize.
Definition 2
Given two LTSs A and B such that \(\varSigma _A \cap \varSigma _B = \varGamma \), the synchronous product of A and B is \(A \parallel B = (S_A \times S_B, \varSigma _A \cup \varSigma _B, \rightarrow _{A \parallel B}, \langle {\imath _A},{\imath _B}\rangle )\), where \(\rightarrow _{A \parallel B}\) is as follows:
Consider again the LTSs A and B of Fig. 2. Their synchronous product \(A \parallel B\) (with \(\varGamma = \{s,t\}\)) is depicted in Fig. 3. \(\square \)
Fig. 2.
From left to right, two UAVs adding to (A) and removing from (B) the buffer.
Next, we generalize the natural projection on languages, which is a kind of inverse operation of the synchronous product of two LTSs. Given a computation of \(A \parallel B\), the natural projection extracts the relevant trace of one of the LTSs, including the synchronized transitions (see the second case below). Note that, unlike the definition given, for example in [33], our definition returns a sequence of transitions, including both states and actions. We also define the inverse projection in the expected way.
Definition 3
For LTSs A and B with \(\varGamma = \varSigma _A \cap \varSigma _B\), the natural projection on A of a trace \(\sigma \), in symbols \(P_{A}({\sigma })\), is defined as follows:
Natural projection on second component B is analogously defined. We extend the natural projection to sets of traces in the usual way: \(P_{A}({T}) = \{P_{A}({\sigma }) \mid \sigma \in T\}\).
The inverse projection of a trace \(\sigma \) over an LTS \(A \parallel B\), in symbols \(P^{-1}_{A}({\sigma })\), is defined as \(P^{-1}_{A}({\sigma }) = \{ \sigma ' \mid P_{A}({\sigma '}) = \sigma \}\). Its extension to sets is \(P^{-1}_{A}({T}) = \bigcup \limits _{\sigma \in T} P^{-1}_{A}({\sigma })\). \(\square \)
Example 5
Consider the two traces \(\sigma _1 = \langle {q_0},{r_0}\rangle \mathbf{d} \langle {q_1},{r_0}\rangle \mathbf{u} \langle {q_1},{r_1}\rangle \mathbf{d} \langle {q_2},{r_1}\rangle \mathbf{s} \langle {q_0},{r_0}\rangle \) and \(\sigma _2 = \langle {q_0},{r_0}\rangle \mathbf{u} \langle {q_0},{r_1}\rangle \mathbf{d} \langle {q_1},{r_1}\rangle \mathbf{d} \langle {q_2},{r_1}\rangle \mathbf{s} \langle {q_0},{r_0}\rangle \). We have that the projections \(P_{A}({\sigma _1}) = P_{A}({\sigma _2}) = q_0 \mathbf{d} q_1 \mathbf{d} q_2 \mathbf{s} q_0 \in [\![{A}]\!]_{}^{}\), and \(\sigma _1, \sigma _2 \in P^{-1}_{B}({q_0 \mathbf{d} q_1 \mathbf{d} q_2 \mathbf{s} q_0})\). Also notice that all the traces of the form \((\langle {q_0},{r_0}\rangle \mathbf d )^*\sigma _1\) belong to \(P^{-1}_{B}({q_0 \mathbf{d} q_1 \mathbf{d} q_2 \mathbf{s} q_0})\). \(\square \)
Two classical properties [33] concerning the interplay between the synchronous product and the natural projection hold, the proofs of which are trivial.
2.3 Equational \(\mu \)-calculus and Partial Model Checking
Below, we recall the variant of \(\mu \)-calculus commonly used in partial model checking called modal equations [1]. A specification is given as a sequence of modal equations, and one is typically interested in the value of the top variable that is the simultaneous solution to all the equations. Equations have variables on the left-hand side and assertions on the right-hand side. Assertions are built from the boolean constants \( ff \) and \( tt \), variables x, boolean operators \(\wedge \) and \(\vee \), and modalities for necessity \([{ \cdot }]\) and possibility \(\langle { \cdot }\rangle \). Equations also have fix-point operators (minimum \(\mu \) and maximum \(\nu \)) over variables x, and can be organized in equation systems.
Definition 4
(Syntax of the\(\mu \)-calculus). Given a set of variables \(x \in X\) and an alphabet of actions \(a \in \varSigma \), assertions\(\varphi , \varphi ' \in \mathcal A\) are given by the syntax:
An equation is \(x =_{\pi } \varphi \), where \(\pi \in \{\mu , \nu \}\), \(\mu \) denotes a minimum fixed point equation, and \(\nu \) a maximum one. An equation system\(\varPhi \) is a possibly empty sequence (\(\epsilon \)) of equations, where each variable x occurs in the left-hand side of at most a single equation. Thus \(\varPhi \) is given by
A top assertion\(\varPhi \!\downarrow \!x\) projects the simultaneous solution of an equation system \(\varPhi \) onto the top variable x. \(\square \)
We define the semantics of modal equations in terms of the traces of an LTS by extending the usual state semantics of [1] as follows. First, given an assertion \(\varphi \), its state semantics \(\Vert {\varphi }\Vert _{\rho }^{}\) is given by the set of states of an LTS that satisfy \(\varphi \) in the context \(\rho \), where the function \(\rho \) assigns meaning to variables. The boolean connectives are interpreted as intersection and union. The possibility modality \(\Vert {\langle {a}\rangle {\varphi }}\Vert _{\rho }^{}\) (respectively, the necessity modality \(\Vert {[{a}]{\varphi }}\Vert _{\rho }^{}\)) denotes the states for which some (respectively, all) of their outgoing transitions labeled by a lead to states that satisfy \(\varphi \). For more details on \(\mu \)-calculus see [8, 22].
Definition 5
(Semantics of the\(\mu \)-calculus [1]). Let A be an LTS, and \(\rho : X \rightarrow 2^{S_A}\) be an environment that maps variables to sets of A’s states. Given an assertion \(\varphi \), the state semantics of \(\varphi \) is the mapping \(\Vert {\cdot }\Vert _{}^{}: {\mathcal A} \rightarrow (X \rightarrow 2^{S_A}) \rightarrow 2^{S_A}\) inductively defined as follows.
×
We extend the state semantics from assertions to equation systems. First we introduce some auxiliary notation. The empty mapping is represented by \([\,]\), \([x \mapsto U]\) is the environment where U is assigned to x, and \(\rho \circ \rho '\) is the mapping obtained by composing \(\rho \) and \(\rho '\). Given a function f(U) on the powerset of \(S_A\), let \(\pi U. f(U)\) be the corresponding fixed-point. We now define the semantics of equation systems by:
×
Finally, for top assertions, let \(\Vert {\varPhi \downarrow x}\Vert _{}^{}\) be a shorthand for \(\Vert {\varPhi }\Vert _{[\,]}^{}(x)\). \(\square \)
Note that whenever we apply function composition \(\circ \), its arguments have disjoint domains. Next, we present the trace semantics: a trace starting from a state s satisfies \(\varphi \) if s does.
Definition 6
Given an LTS A, an environment \(\rho \), and a state \(s \in S_A\), the trace semantics of an assertion \(\varphi \) is a function \(\langle \!\langle {\cdot }\rangle \!\rangle _{}^{}: {\mathcal A} \rightarrow S_A \rightarrow ( X \rightarrow 2^{S_A}) \rightarrow {\mathcal T}\), which we also extend to equation systems, defined as follows.
We write \(\langle \!\langle {\varPhi \!\downarrow \!x}\rangle \!\rangle _{}^{}\) in place of \(\langle \!\langle {\varPhi }\rangle \!\rangle _{[\,]}^{}(x)\). \(\square \)
Since \(U^2 = U^3\), we have obtained the fixed point \(U^*\). Finally, we can compute \(\langle \!\langle {\varPhi \!\downarrow \!x}\rangle \!\rangle _{}^{}\), which amounts to \( [\![{A,\langle {q_0},{r_0}\rangle }]\!]_{}^{} \cup [\![{A,\langle {q_2},{r_0}\rangle }]\!]_{}^{} \). \(\square \)
We now define when an LTS satisfies an equation system. Recall that \([\![{A}]\!]_{}^{}\) stands for \([\![{A,\imath _A}]\!]_{}^{}\).
Definition 7
An LTS A satisfies a top assertion \(\varPhi \!\downarrow \!x\), in symbols , if and only if \(\imath _A \in \Vert {\varPhi \!\downarrow \!x}\Vert _{}^{}\). Moreover, let if and only if \([\![{A}]\!]_{}^{} \subseteq \langle \!\langle {\varPhi \!\downarrow \!x}\rangle \!\rangle _{}^{}\). \(\square \)
The following fact relates the notion of satisfiability defined in terms of state semantics (\(\models _s\)) with the one based on trace semantics (\(\models _\sigma \)); its proof is immediate by Definition 6.
Fact 2
if and only if .
As previously mentioned, partial model checking is based on the quotienting operation \({}/\!\!/_{\!}{}\). Roughly, the idea is to specialize the specification of a composed system on a particular component. Below, we define the quotienting operation [1] on the LTS \(A \parallel B\). Quotienting reduces to solving . Note that each equation of the system \(\varPhi \) gives rise to a system of equations, one for each state \(s_i\) of A, all of the same kind, minimum or maximum (thus forming a \(\pi \)-block [3]). This is done by introducing a fresh variable \(x_{s_i}\) for each state \(s_i\). Intuitively, the equation represents the requirements on B when A is in state \(s_i\). Since the occurrence of the variables on the right-hand side depends on the A’s transitions, embeds the behavior of A.
Definition 8
Given a top assertion \(\varPhi \downarrow x\), we define the quotienting of the assertion on an LTS A with respect to an alphabet \(\varSigma _B\) as follows.
\(\square \)
Example 7
Consider the top assertion \(\varPhi \downarrow x\) of Example 6 and the LTSs A and B of Example 3. Quotienting \(\varPhi \downarrow x\) against B, we obtain where
The leftmost equations are obtained by applying the rules of Definition 8. Then we simplify on the right-hand sides. Finally we reduce the number of equations by removing those unreachable from the top variable \(x_{r_0}\). For a detailed description of our simplification strategies we refer the reader to [3]. By proceeding as in Example 6, we obtain \( \{q_0, q_2, q_3\}\) as the fixpoint. \(\square \)
3 Unifying the Logical and the Operational Approaches
In this section we prove the equivalence between natural projection and partial model checking (Theorem 4). To start, we introduce an auxiliary definition that roughly acts as a quotienting of an environment \(\rho \). Below, we will write \(\bigoplus \limits _{i \in I} \rho _i\) for the finite composition of functions \(\rho _i\) over the elements of an index set I.
Definition 9
Given a synchronous product \(A \parallel B\), we define
A technical lemma follows. Intuitively, quotienting an assertion (and an environment) preserves the semantics, i.e., a state \(\langle {s_A},{s_B}\rangle \) satisfies \(\varphi \) if and only if \(s_B\) satisfies the quotient of \(\varphi \) on B. Indeed, the following statement can be rewritten as .
Lemma 1
For all \( A, B, \rho \) and \(\varphi \) on \(A \parallel B\), .
We next extend Lemma 1 to a system of equations, providing an alternative view of quotienting an assertion on a component of a synchronous product.
Lemma 2
For all \( A, B, \rho \) and \(\varPhi \) on \(A \parallel B\),
The following corollary is immediate (recall that \(x_{s_A}\) is the variable corresponding to the quotient of x on \(s_A\)).
Corollary 1
For all \( A, B, \rho , x\) and \(\varPhi \) on \(A \parallel B\),
We next establish the correspondence between quotienting and natural projection.
Theorem 3
For all A, B, x and \(\varPhi \) on \(A \parallel B\),
The following theorem states that the synchronous product of two LTSs satisfies a global equation system if and only if its components satisfy their quotients, i.e., their local assertions.
Theorem 4
For all A, B, x and \(\varPhi \) on \(A \parallel B\),
$$ A \parallel B \, \models _\varsigma \, \varPhi \!\downarrow \!x \qquad (\varsigma \in \{ s, \sigma \}) $$
if and only if any of the following equivalent statements holds:
In this section we present an algorithm for quotienting a finite-state system defined as an LTS. Afterwards, we prove its correctness with respect to the standard quotienting operator and we study its complexity. Finally, we apply it to our working example to address three problems: verification, submodule construction, and controller synthesis.
4.1 Quotienting Algorithm
Our algorithm consists of two procedures that are applied sequentially. The first, called quotient (Table 2), builds a non-deterministic transition system from two LTSs, i.e., a specification P and an agent A. Moreover, it takes as an argument the alphabet of actions of the new transition system. Non-deterministic transition systems have a distinguished label \(\lambda \), and serve as an intermediate representation. The states of the resulting transition system include all the pairs of states of P and A, except for those that denote a violation of P (line 1). The transition relation (line 3) is defined using the quotienting rules from Sect. 2. Also, note that the relation \(\rightarrow \) is restricted to the states of S (denoted \(\rightarrow _S\)).
The second procedure, called unify (given in Table 3) translates a non-deterministic transition system back to an LTS. Using closures over \(\lambda \), unify groups states of the transition system. This process is similar to the standard subset construction algorithm [19], except that we put an \(a \in \varSigma _B \setminus \varGamma \) transition between two groups Q and M only if (i) M is the intersection of the \(\lambda \)-closures of the states reachable from Q with an a transition and (ii) all the states of Q admit at least an a transition leading to a state of M (\(\wedge \)-move). Procedure unify works as follows. Starting from the \(\lambda \)-closure of B’s initial state (line 1) it repeats a partition generation cycle (lines 4–13). Each cycle removes an element Q from the set S of the partitions to be processed. Then, for all the actions in \(\varSigma _B \setminus \{ \lambda \}\), a partition M is computed by \(\wedge \)-move (line 7). If the partition is nonempty, a new transition is added from Q to M (line 9). Also, if M is a freshly generated partition, i.e., \(M \not \in R\), it is added to both S and R (line 10). The procedure terminates when no new partitions are generated.
Table 2.
The quotienting algorithm.
Table 3.
The unification algorithm.
Our quotienting algorithm is correct with respect to the quotienting operator and runs in PTIME. Intuitively, we avoid an exponential blow-up in our contribution (in contrast to Table 1) since we only consider deterministic transition systems. Notice that a determinization step for non-deterministic transition systems is exponential in the worst case.
4.2 Prototype and Application to the Running Example
We implemented the algorithm presented above as part of a tool suite for the partial evaluation of finite state models called the partial evaluator of simple transition systems (pests).1 We applied the prototype to some case studies, including a real world one based on a flexible manufacturing system.2 For the sake of presentation we only show here the application to the running example. In particular, we leverage our algorithm to address three different problems: (i) reducing the verification of a parallel composition to that of a single component, (ii) synthesizing a submodule that respects a global specification (SCP), and (iii) synthesizing a controller for a given component (CSP).
Verification. Here we want to check whether . To do this we follow the approach of [1], i.e., we start by quotienting the specification P(2) against A (see Fig. 2). The result is a two-state specification \(P'\) having a single transition labeled with t. Clearly and a counterexample is the trace \(\sigma = \mathbf{r_0} u \mathbf{r_1} s \mathbf{r_0} t \mathbf{r_2}\), as \(\sigma \in [\![{B}]\!]_{}^{}\) while \(\sigma \not \in [\![{P'}]\!]_{}^{}\). As a consequence . Intuitively, this is because after the two d actions, A performs a single s, which is insufficient to delimit a “safety zone” for actions u by B (which might occur too late, e.g., after another d by A). Thus, \(P'\) does not allow an s that might permit A to carry out the third d move before a u action.
Fixing the example. Given to the previous reasoning, we cannot synthesize meaningful submodules and controllers starting from A. To fix our example, we therefore replace A with \(A'\), as depicted in Fig. 4. \(A'\) resembles A but has an extra state \(q_4\) that enables a second s transition. Intuitively, it represents the “safety zone” just described.
SCP. We now apply the quotienting algorithm to \(A'\) in the case of buffer sizes 2 and 3 to construct the submodules that comply with P(2) and P(3), respectively. Thus, we set \(\varSigma _B = \{ u, s, t\}\). In this way, the quotienting algorithm generates a component that not only synchronizes through actions s and t, but also performs actions u autonomously. The resulting agents \(B_2\) and \(B_3\) appear in Fig. 4.
Fig. 4.
Graphical representation of \(A'\), \(B_2\) and \(B_3\) (from left to right).
×
The agent \(B_2\) synchronizes on the first s transition of \(A'\) to ensure that both the d actions have been performed. Afterwards, the buffer must be cleared (two u actions) before synchronizing again on s (thereby permitting \(A'\) to cycle). Synchronizing on t is also possible. In this case, no further modifications of the buffer happen.
With a buffer of size 3, the agent \(B_3\) is more complex. Intuitively, \(A'\) can perform its two d actions only when the buffer contains at most one item. Thus, \(B_3\) has two loops. The inner loop (passing through the states \(w_0\,w_1\,w_2\,w_4\)) is analogous to that of \(B_2\) (where two u actions are performed in sequence) and, if completed, it empties the buffer. Moreover, the specification includes an external loop (\(w_2\,w_3\,w_6\,w_1\)) that removes two elements from the full buffer of size 3. As expected, the two cycles can be combined. Finally, notice that the action t can occur under two conditions: if the buffer contains no items (\(w_0\)) or exactly 1 item (\(w_3\)). In the second case, a final u action (\(w_5\)) can occur.
Fig. 5.
Graphical representation of \(A'\parallel B_3\) and C (from left to right).
×
CSP. We consider now the problem of synthesizing a controller for \(A' \parallel B_3\) (see Fig. 5). In particular, we want a controller to enforce P(2) on it.3 To generate the controller, we run the quotienting algorithm with \(\varSigma _B = \{s, t\}\), i.e., we force the algorithm to build a component that can only synchronize on the controllable actions s and t. The resulting controller is depicted on the right of Fig. 5. Intuitively, the controller only admits two operations: either t or s. The first case is when \(A'\) and \(B_3\) terminate (state \(\langle {q_4},{w_7}\rangle \)). Otherwise, only a single s action can occur. In fact, after one s action, the target reaches \(\langle {q_3},{w_1}\rangle \) completely filling in the stack with two d actions. The system can then reach both \(\langle {q_3},{w_2}\rangle \) and \(\langle {q_3},{w_4}\rangle \). Since an s action leads from \(\langle {q_3},{w_2}\rangle \) to \(\langle {q_0},{w_3}\rangle \), where the system can perform other two d transitions, it is not allowed.
5 Related Work
Natural projection is mostly used by the community working on control theory and discrete-event systems. In the 1980s, the seminal works by Wonham et al. (e.g., [34, 35]) exploited natural projection-based algorithms for synthesizing both local and global controllers. Along this line of research, other authors proposed extensions and refinements, relying on natural projection (e.g., see [13, 14, 24, 32]).
Partial model checking has been successfully applied to the synthesis of controllers. Given an automaton representing a plant and a \(\mu \)-calculus formula, Basu and Kumar [6] compute the quotient of the specification with respect to the plant. The satisfiability of the resulting formula is checked using a tableau that also returns a valid model yielding the controller. Their tableau works similarly to our quotienting algorithm, but applies to a more specific setting, as they are interested in generating controllers. In contrast, Martinelli and Matteucci [26] use partial model checking to generate a control process for a partially unspecified system in order to guarantee the compliance against a \(\mu \)-calculus formula. The generated controller takes the form of an edit automaton [7].
Some authors proposed techniques based on the formal verification of temporal logics for addressing CSP. Arnold et al. [4] were among the first to control a deterministic plant with a \(\mu \)-calculus specification. Also Ziller and Schneider [36] and Riedwge and Pinchinat [29] reduce the problem of synthesizing a controller to check the satisfiability of a formula of (a variant of) the \(\mu \)-calculus. A similar approach was presented by Jiang and Kumar [20] and Gromyko et al. [17]. Similarly to [20, 29, 36] puts forward an approach that reduces the problem of synthesizing a controller to that of checking a CTL\(^\star \) formula’s satisfiability. In contrast, [17] proposes a method based on symbolic model checking to synthesize a controller. Their approach applies to a fragment of CTL.
6 Conclusion
Our work goes in the same direction of [12] and provides results that build a new bridge between supervisory control theory and formal verification. In particular, we have formally established the relationship between partial model checking and natural projection by reducing natural projection to partial model checking and proving them equivalent under common assumptions. This equivalence helps explain why some authors use partial model checking and others use natural projection to synthesize controllers. We have also developed a working prototype that we haven applied to our running example and to a realistic case study.
Besides establishing an interesting and novel connection, our work also opens new directions for investigation. Since natural projection is related to language theory in general, there could be other application fields where partial model checking can be used as an alternative. The original formulation of partial model checking applies to the \(\mu \)-calculus, while our quotienting algorithm works on LTSs. To the best of our knowledge, no quotienting algorithms exist for formalisms with a different expressive power, such as LTL or CTL.
This work was partially supported by SNSF funded project IZK0Z2_168370 “Enforceable Security Policies in Fog Computing” and by CINI Cybersecurity National Laboratory within the project FilieraSicura: Securing the Supply Chain of Domestic Critical Infrastructures from Cyber Attacks (www.filierasicura.it) funded by CISCO Systems Inc. and Leonardo SpA.
<SimplePara><Emphasis Type="Bold">Open Access</Emphasis> This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.</SimplePara>
<SimplePara>The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.</SimplePara>
Natural projection on second component B is analogously defined. We extend the natural projection to sets of traces in the usual way: \(P_{A}({T}) = \{P_{A}({\sigma }) \mid \sigma \in T\}\).
, if and only if \(\imath _A \in \Vert {\varPhi \!\downarrow \!x}\Vert _{}^{}\). Moreover, let
if and only if \([\![{A}]\!]_{}^{} \subseteq \langle \!\langle {\varPhi \!\downarrow \!x}\rangle \!\rangle _{}^{}\). \(\square \)
if and only if
.
to solving
. Note that each equation of the system \(\varPhi \) gives rise to a system of equations, one for each state \(s_i\) of A, all of the same kind, minimum or maximum (thus forming a \(\pi \)-block [3]). This is done by introducing a fresh variable \(x_{s_i}\) for each state \(s_i\). Intuitively, the equation
represents the requirements on B when A is in state \(s_i\). Since the occurrence of the variables on the right-hand side depends on the A’s transitions,
embeds the behavior of A.
\(\square \)
whereThe leftmost equations are obtained by applying the rules of Definition 8. Then we simplify on the right-hand sides. Finally we reduce the number of equations by removing those unreachable from the top variable \(x_{r_0}\). For a detailed description of our simplification strategies we refer the reader to [3]. By proceeding as in Example 6, we obtain \( \{q_0, q_2, q_3\}\) as the fixpoint. \(\square \)
.
.
2.
. To do this we follow the approach of [1], i.e., we start by quotienting the specification P(2) against A (see Fig. 2). The result is a two-state specification \(P'\) having a single transition labeled with t. Clearly
and a counterexample is the trace \(\sigma = \mathbf{r_0} u \mathbf{r_1} s \mathbf{r_0} t \mathbf{r_2}\), as \(\sigma \in [\![{B}]\!]_{}^{}\) while \(\sigma \not \in [\![{P'}]\!]_{}^{}\). As a consequence
. Intuitively, this is because after the two d actions, A performs a single s, which is insufficient to delimit a “safety zone” for actions u by B (which might occur too late, e.g., after another d by A). Thus, \(P'\) does not allow an s that might permit A to carry out the third d move before a u action.