ough systems with process creation give rise to unboundedly many processes, their names are systematically generated and typically form a regular set. When we consider modal logics to specify properties of such systems, it is natural to consider quantication over such regular sets. ese are in the realm of term modal logics, which are usually undecidable. We consider the monodic variant, in which there is only one free variable in the scope of any modality, and present a model checking algorithm for this logic.
Modal logic, and its variants including temporal logics play an
important role in system verication[
We illustrate this using an example.
Example 1.1. Consider an operating system which can execute many processes at a time. A conguration of the system is given by the states of its active processes. Any active process can change the system state by making a move. Let us assume that a move by a process can create one or more new processes (threads), thus making the active set dynamic and potentially unbounded. In this seing, we can consider assertions such as: there is at least one process active in the present conguration or for all possible next congurations, the processes that are currently active will remain active in the next : : : ese cannot be expressed in modal logics with xedly many modalities.
One solution is to consider a modal logic with innitely many modalities. For instance, ^nα may be read as “process n makes a Copyright ©2017 for the individual papers by the papers’ authors. Copying permied for private and academic purposes. is volume is published and copyrighted by its editors. transition to a state satisfying α ”, where n is any natural number. However, a simple exercise shows that a formula in the logic can force only boundedly many agents and hence models are systems with xedly many agents. Also, it is not possible to state properties like “there exists a process such that ” since it needs an innite disjunction. So we need another logical device to force unboundedly many agents.
A natural such logical mechanism is quantification. It is possible
to express all the properties of the kind mentioned above using rst
order modal logic[
Perhaps what ts us best are the term modal logics (T ML)
introduced by Fiing, almann and Voronkov [
Note that T ML is dierent from standard rst order modal logic,
since in T ML quantied variables are allowed as indices for
modalities which is not the case in rst order modal logics. Term modal
logic oers an intuitive way to talk about unboundedly or countably
many agents and gives us a device to quantify over them. Fiing
et :al in [
Since the logic is undecidable, we focus on the monodic fragment:
formulas in which only one free variable occurs in the scope of any
modality. In [
Denition 2.1. Given a countable set of propositions P , and a countable set of variables V ar , the syntax is dened as follows: ϕ := p 2 P j :ϕ j ϕ ^ ϕ j ^x α j 9xα ;x 2 V ar where FV (α )
fx g.
e notion of free variable of a formula (referred to in the syntax) is standard. FV (p) = ;, for p 2 P . FV (:ϕ) = FV (ϕ). FV (ϕ ^ ψ ) = FV (ϕ) [ FV (ψ ). FV (^x ϕ) = FV (ϕ) [ fx g. FV (9x ϕ) = FV (ϕ) n fx g. We call a formula ϕ a sentence if FV (ϕ) = ;.
Similarly the modal depth of ϕ, denoted md (ϕ) is dened inductively: md (p) = 0, for p 2 P . md (:ϕ) = md (ϕ). md (ϕ ^ ψ ) = max fmd (ϕ);md (ψ )g. md (^x ϕ) = md (ϕ) + 1. md (9x ϕ) = md (ϕ).
As one would expect, Kripke models now need to be enriched with interpretations for variables over agent names. In addition, agent dynamics is captured by a function (γ below) that species, at any world w, the set of agents alive (or meaningful) at w. en coherence demands that whenever (u;d;v ) 2 R, we have that d 2 γ (u ).
Denition 2.2. A model is a tuple M = (W ; D; R;γ ; I ;V ) where W is a non-empty set of worlds, D is a non-empty set of names, R W D W , γ : W ! 2D , I : V ar ! D, V : W ! 2P . Moreover, for all u 2 W and d 2 D, if there exists v 2 W such that (u;d;v ) 2 R, then d 2 γ (u ).
In [
We will oen display the model as M = (F ; I ) where F = (W ; D; R;γ ;V ) is referred to as a frame. Sometimes we denote (u;d;v ) by u !d v.
Given a formula ϕ and a model M = (W ; D; R;γ ; I ;V ), for any w 2 W we dene M;w j= ϕ (ϕ is true at w) inductively as follows: M;w j= p if p 2 V (w ).
M;w j= :ϕ if M;w 6j= ϕ.
M;w j= ϕ1 ^ ϕ2 if M;w j= ϕ1 and M;w j= ϕ2.
M;w j= ^x ϕ if there is some u 2 W such that (w; I (x );u ) 2 R and M;u j= ϕ.
M;w j= 9x ϕ if there is some d 2 γ (w ) such that Mx !d ;w j= ϕ where Mx !d is dened by (W ; D; R;γ ; I 0;V ) such that for any y , x ; I 0(y) = I (y) and I 0(x ) = d.
e boolean connectives, x ϕ and 8xϕ are dened in the standard way. A formula ϕ is satisable if there is some model and some world w such that ϕ is true at w.
Example revisited. We show some properties in the example system 1.1 discussed earlier, using formulas of the proposed logic. ere is at least one process active which can potentially change the system state: 9x ^x >.
For all possible next congurations, property p holds: 8x ( x p). ere are at least two processes active: 9x x p ^ 9y ^y :p 1. 1x and y cannot have same witness hence at least two processes are required. ere is a process such that it can change to a conguration in which none of the processes can make a move (system halts): 9x ^x 8y y ?.
Note that all the properties discussed could be expressed in the monodic fragment of the logic. 3
Systems with unboundedly many processes to be model checked are presented as transition systems with nitely many states and edges between the states labelled by regular expressions. e idea is that there is a nite alphabet set and every process name is some string over this alphabet. If a string s is in the language of some regular expression r and there is an r edge from q to q0 then it means that process s can change the system state from q to q0.
Denition 3.1. Let Σ be a nite alphabet. Let Reg(Σ) be the set of all regular expressions over Σ. For all r 2 Reg(Σ) let Lr denote the regular language generated by the expression r . If s;t 2 Σ then s t denotes the concatenation of strings s and t , oen wrien st .
A regular agent transition system is given by T = (Q;S;δ ;q0) where
S f in Reg(Σ) is a nite set of regular expressions, δ (Q S Q ) and q0 2 Q.
f in (Q
Reg(Σ) Q ) and extracted S from δ . Note that when we have u1 r!1 u2 r!2 u3 2 R1 with a 2 Lr1 and ab 2 Lr2 we could think of b as a child process of parent process a. e language of regular expressions is rich enough to consider tree structures of concurrent and sequential threads with forking, as well as process threads created within loops, perhaps while waiting for an external event to occur.
Denition 3.2. Given a nite set of regular expressions S over Σ, for any two strings s;t 2 Σ , dene s t if for all r 2 S, s 2 Lr i t 2 Lr .
Note that induces a partition of Σ . For all strings s 2 Σ , dene ~s = ft j s t g. We denote this by T . 3.1
e input for model checking is specied by the tuple (T ;ϕ; I ;U ;s0) where T is a regular agent transition system as dened above, ϕ is a monodic formula I : FV (ϕ) ! Σ , U : Q ! 2Pϕ and s0 2 Σ . is induces the following model on which the model checking is done.
Denition 3.3. Given an input (T ;ϕ; I ;V ;s0), dene the induced frame FT = (W ; D; R;γ ;V 0) as follows:
D = Σ W (Q Σ ) and R (W D W ) are the least sets such that the following conditions hold: – (q0;s0) 2 W . – if (q;s ) 2 W and (q;r ;q0) 2 δ then (q0;st ) 2 Q and
(q;s ); t ; (q0;st ) 2 R where st 2 Lr . for all (q;s ) 2 W , γ ((q;s )) = fs g [ ft 2 Σ j for some q0 we have (q;s );t ; (q0;st ) 2 Rg. for all (q;s ) 2 W , V ((q;s ) = U (q).
e clause dening γ needs some explanation. It species the set of active agents at a node to be exactly those that have some transitions; these agents surely need to be active but do we not need more ? For instance, what about inheriting already active agents at parent nodes ? e answer is that for monodic formulas, there is only one variable free at any node and hence the children “created” are all forced only by bound variables, and once we have substituted for the free variables at the root, we do not need any further inheritance. us the denition here suces.
Given an input instance (T ;ϕ;I ;V ;s0), the model checking problem is to decide whether (FT ;I ); (q0;s0) j= ϕ.
Note that it is enough to consider a tree frame which is the unravelling of FT upto depth md (ϕ) with (q0;s0) as the root. Hence the model checking problem is on a rooted tree with bounded depth but can have potentially innite branching. Let the induced tree model be M(T ;ϕ;I;V ;s0) = (W ; D;R;γ ;I ;V ), the corresponding rooted tree, with Wi being the set of all nodes at level i, where W0 = (q0;s0).
Consider the example 1.1. We now illustrate the model checking problem for a system of this kind. Let the system processes be named by strings over Σ = fa;bg. Let the regular agent transition system T be as given in the gure 1.
q0 r1 r2 r1 q1 q2 r2
r1
Suppose r1 = Σ a and r2 = (ab) , then the induced model is given in gure 2. e set of processes active at any state is given by the union of the labels of outgoing edges from the corresponding state. For instance, γ (q0;ϵ ) = fϵ;a;ab g.
Now, if the model checking is to be done at the node (q2;ϵ ), then the corresponding unravelled tree is given in g 3.
q2;ϵ ϵ q2;ϵ
a q0;a ϵ q2;ϵ q0;a a a q1;aa ba q0;ba a q1;baa
Now suppose the valuation functions are given by V (q0) = fpg, V (q1) = fp;r g and V (q2) = fr g then 8x x (p ^ r ) is false at (q2;ϵ ) however, 9x ^x ^x (p ^ r ) is true at (q2;ϵ ).
Before addressing the model checking problem, we dene the notion of bisimulation.
Denition 4.1. Given two frames F1 = (W1; D1;R1;γ1;V1) and F2 = (W2; D2; R2;γ2;V2), we dene a tuple (G;H ) to be a bisimulation where G is called world bisimulation with G W1 W2 and H D1 D2 is called name bisimulation such that for any (u1;u2) 2 G the following conditions hold:
V1 (u1) = V2 (u2). for any d1 2 γ1 (u1) there is some d2 2 γ2 (u2) such that (d1;d2) 2 H . for any d2 2 γ2 (u2) there is some d1 2 γ1 (u1) such that (d1;d2) 2 H . for every d1 2 D1 and v1 2 W1 if u1 d!1 v1 2 R1 then for every d2 2 D2 if (d1;d2) 2 H then there exists v2 2 W2 such that (v1;v2) 2 G and u2 d!2 v2. for every d2 2 D2 and v2 2 W2 if u2 d!2 v2 2 R2 then for every d1 2 W1 if (d1;d2) 2 H then there exists v1 2 W1 such that (v1;v2) 2 G and u1 d!1 v1.
It is an easy exercise to show that formulas of our logic preserve
bisimulation ([
Denition 4.2. For any given input instance (T ;ϕ; I ;V ;s0), consider the induced tree model M(T ;ϕ;I;V ;s0) = (W ; D; R;γ ; I ;V ). For every height i md (ϕ) and for all (q;s ); (q0;s 0) 2 Wi dene (q;s ) ui (q0s 0) if q = q0, and s T s 0 .
u induces a partition of W . Dene [(q;s )] = f(q0;s 0) j (q;s ) u (q0;s )g and W 0 = f[(q;s )] j (q;s ) 2 W g.
Dene D 0 = f[s] j s 2 Σ g.
For that ui and T induce a bounded partition and the size of jD 0j 2jS j and jW 0j l 2 2jS j jQ j where Q and S are the nite set of states and nite set of regular expressions specied in T respectively and l is the length of the formula ϕ.
Denition 4.3. Given an input instance (T ;ϕ; I ;V ;s0), consider the induced tree model M(T ;ϕ;I;V ;s0) = (W ; D; R;γ ; I ;V ). Dene the ltered model M(0T ;ϕ;I;V ;s0) = (W 0; D 0; R0;γ 0; I 0;V 0) as follows:
R0 = f [(q;s )]; [t ]; [(q0;st )] j (q;s );t ; (q0;st ) 2 Rg. γ 0([(q;s )]) = f[t ] j t 2 γ (q;s )g.
For any variable x , if I (x ) = t then I 0(x ) = [t ].
V 0([(q;s )] = V ((q;s )).
First we observe that given a nite model M, there are only nitely
many agents used as names in the model and hence the standard
labelling algorithm for model checking modal logics can be used [
Theorem 4.4. Given an input instance (T ;ϕ; I ;V ;s0), consider the induced model M = (W ; D; R;γ ; I ;V ) and the ltered model M 0 = (W 0; D 0; R0;γ 0; I 0;V 0). en, for all (q;s ) 2 W we have (q;s ) 2 Wi is bisimilar to [(q;s )] 2 Wi0.
Proof. Dene G = f (q;s ); [(q;s )] j (q;s ) 2 W where (q;s ) and [(q;s )] are at same level g and H = f(t ; ~t ) j t 2 Σ g. We show that (G; H ) is a bisimulation by verifying all the required properties. e rst property is satised since by denition V 0([(q;s]) = V (q;s ).
Suppose t 2 γ (q;s ) then by denition ~t 2 γ 0([q;s]). For the third property, rst we observe the following: suppose t 2 γ ((q;s )); then there is some r such that t 2 Lr and (q;r ;q0) 2 δ for some q0. Hence for any (q1;s1) u (q;s ) we have t 2 γ ((q1;s1) because by denition q1 = q and s T s1.
Now suppose that ~t 2 γ 0([(q;s )]); we need to prove that t1 2 γ (q;s ) for some t 0 T t . Since ~t 2 γ 0([(q;s )]) there is some t2 2 ~t and some (q0;s 0) 2 [(q;s )] such that t2 2 γ (q0;s 0) then by the observation above, for all (q1;s1) 2 [(q;s )] we have t2 2 γ ((q1;s1).
Suppose (q;s );t ; (q0;st ) 2 R then by denition [(q;s )]; [t ]; [(q0;st )] 2 R0. For the last condition, suppose [(q;s )]; ~t ; [(q0;st )] 2 R0; let (q;s1) 2 [(q;s )] we need to prove that there is some t1 2 ~t such that (q0;s1t1) u (q;st ).
By denition there is some t2 2 ~t , (q;s2) 2 [(q;s )] and (q0;s20t2) 2 [(q0;s2t2)] such that (q;s2);t2; (q0;s2t2) 2 R. Since s1 s2 and t1 t we have s1t s2t and thus (q0;s1t ) u (q0;st ). Now, by denition (q;s1);t ; (q0;s1t1) 2 R and hence we are done.
Hence (q;s ) in M and [(q;s )] in M 0 at the same level satisfy the same formulas, and we are done.
Theorem 4.5. Given an input instance (T ;ϕ; I ;V ;s0), the corresponding model checking problem is in O (l 2 2jS j jQ j) non deterministic time where l is the length of ϕ and Q and S are the states and regular expressions mentioned in T respectively.
Proof. Construct M 0 which is O (l l 2jS j jQ j) size. is is because the two l factors corresponding to height of the tree and length of the formula and the jS j jQ j factor is due to the number of equivalence paritions. Now, since M 0 is nite, we can check if M 0; [(q0;s0)] j= ϕ in polynomial time (in the size of M 0) and since (q0;s0) in M is bisimilar to [(q0;s0)] 2 M 0, the truth of the formula is preserved.
In this paper, we show that model checking for monodic PT ML over transition systems with regular sets of agents is in non deterministic EX P -time. We do not have a matching lower bound, but with the power of quantication, an exponential cost is rather to be expected. However, it remains to explore the model checking of full PT ML.
Another interesting direction is to use dynamic logic (for regular sets of names) over modalities rather than quantication.
On the systems side, the most important line to pursue is to have a processes specied by a term algebra with process creation, and consider model checking of such processes directly. One would then naturally be led to process termination as well. However, it remains to be seen how far monodic specications will be useful for verifying properties of such systems. Perhaps more interesting would be constraints on such systems as well as structure on formulas that yield beer algorithmic properties for model checking.
We thank the reviewers for many insightful comments which have given us interesting directions for further development of this work.‘