We show that the vectorial -calculus model checking problem over arbitrary graphs reduces to the vectorial, existential -calculus model checking problem over S5 graphs. We also draw some consequences of this fact. Moreover, we give a proof that satis ability of -calculus in S5 is N P -complete, and by using S5 graphs we give a new proof that the satis ability problem of the existential -calculus is also N P -complete.
Model checking is a technique widely used in veri cation of computer systems,
be they hardware or software, see [
The model checking technique raises a natural computational question, which
is known as the ( -calculus) model checking problem. Formally, the -calculus
model checking problem is: given a -calculus formula and a nite graph, check
whether the graph satis es the formula. Because of the importance of model
checking in practice, it would be desirable to have an e cient, i.e. polynomial
time computable, model checking algorithm for arbitrary ( nite) graphs, but this
algorithm has not been found. We know that the problem is in the complexity
class U P , see [
The other main theme of this paper is given by S5 graphs, i.e. graphs whose relation is an equivalence.
The modal logic of S5 graphs (also called modal logic S5) is important because it is widely recognized as a good epistemic logic, where the box operator [ ] means that some agent knows . When modal logic is interpreted on Kripke structures, i.e. graphs, the vertices of the structure represent possible situations, and it is reasonable that the knowledge of an agent is represented by an equivalence relation on the vertices, which indicates that certain situations are not distinguishable, in the agent's knowledge.
So, S5 is a way of formalizing the ideas of knowledge, and it is used in many applications such as arti cial intelligence, etc. Often multimodal versions of S5 are considered, where di erent agents come into play; in this paper, however, we will focus on a single modality, representing a single agent.
We will consider also the class of all transitive graphs, called K4 in the
modal logic literature. Many interesting relations are transitive: for instance, the
relation \the event A is posterior to the event B" de nes a transitive relation
between events. In this paper K4 graphs play only a minor role; papers dedicated
to the -calculus in K4 are [
In this paper we compare the behavior of the -calculus on arbitrary graphs and on S5 graphs. It is well known that the -calculus is expressively equivalent to modal logic over S5, but this equivalence does not transfer automatically to an equivalence in complexity, neither for model checking, nor for satis ability.
From this perspective we rst show that the -calculus model checking problem for arbitrary graphs is as di cult as the subcase of S5 graphs, although the class of S5 graphs is signi cantly simpler than the class of all graphs.
Then we move to the satis ability problem. Quite generally, recall that the satis ability problem for a logic L on a class of models C is: given a formula in L, decide whether there is a model of which is in C.
The satis ability problem of the -calculus on arbitrary graphs is settled, in
the sense that it is EXP T IM E-complete: EXP T IM E-hardness of the problem
follows from [
Given the relevance of S5 as epistemic logic, many papers in the modal logic
literature are dedicated to it, and in particular on its proof theory. Finding a
good axiom system for S5 is a longstanding open problem, see [
We present here the usual modal -calculus, and we call it scalar because, as we will see, there is also a vectorial version of the -calculus. We follow the standard presentation of the formulas of modal -calculus: = A j :A j X j _ j ^ j h i j [ ] j
X: j
X: ; where A ranges over a set At of atoms and X ranges over a set V ar of xpoint variables. h i and [ ] denote the modal operators: the diamond, or the existential operator, and the box, or the universal operator.
Intuitively, X: (X) denotes the least xpoint of the function (X), and X: (X) denotes the greatest xpoint of this function.
A -calculus formula is called guarded if for every xpoint subformula of , say X: (X) or X: (X), every occurrence of X in is in the scope of a modal operator.
Free and bound variables are de ned in analogy with rst order logic, because xpoints X and X are syntactically analogous to quanti ers 9x and 8x (note however that semantically, xpoint variables correspond to monadic second order variables, i.e. variables ranging over sets, rarther than rst order variables ranging over individuals).
A -calculus formula is called a sentence if it has no free variables. Although formulas are not closed under negation, a negation of sentences is available: the negation of a sentence is obtained by exchanging A and :A, ^ and _, h i and [ ], and with .
Given a formula , we denote by j j the size of . 2.2
We can generalize modal -calculus to functional -calculus, following [
Xj ^ j _ jf ( 1; : : : ; n)j X: j X: : 2.3
The most standard presentation of modal -calculus is in the scalar syntax of the previous section. In this section we generalize the syntax by allowing systems of equations: although this extension does not a ect the expressiveness of the logic, it may increase succinctness.
We essentially follow the presentation of [
8 x1 = 1 f1(x1; : : : ; xn; y1; : : : ; ym) S : < : : :
: xn = n fn(x1; : : : ; xn; y1; : : : ; ym) where 1; : : : ; n 2 f ; g.
The -system S is by de nition equivalent to a n tuple of scalar -calculus formulas, called the solution of S, computed inductively as follows.
If n = 1 then the solution is x1:f1(x1; y1; : : : ; ym).
If n > 1, let g1(x2; : : : ; xn; y1; : : : ; ym) = 1x1:f1(x1; : : : ; xn; y1; : : : ; ym). The solution of S is (g1(h2; : : : ; hn; y1; : : : ; ym); h2; : : : ; hn), where (h2; : : : ; hn) is the solution of the system
S1 : 8 x2 = 2 f2(g1(x2; : : : ; xn; y1; : : : ; ym); : : : ; xn; y1; : : : ; ym) < : : : : xn = n fn(g1(x2; : : : ; xn; y1; : : : ; ym); : : : ; xn; y1; : : : ; ym) We denote by soli(S) the i-th component of the solution of S.
A -system of equations is called a modal -system if all functions fi are combinations of variables, atoms, negated atoms, conjunctions, disjunctions, diamonds, and boxes.
The modal -calculus vectorial model checking problem is: given a nite graph G and a modal -system S, decide whether G satis es sol1(S). 2.4
Given a -system S, we de ne a relation LEF T between the variables of S as follows.
Let y; z two variables of S. We say that y is at left of z, written y LEF T z, if there is an equation of S where y is the variable at the left hand side of the equality and z occurs at the right hand side.
A modal -system is called a modal system if the LEF T relation on variables is acyclic. Every modal system is equivalent to a formula of modal logic. 2.5
Let (X) be a formula containing a free variable X and let be a sentence. Then the composition [X= ] is the formula obtained by replacing X everywhere with in . Note that is a sentence, hence there is no variable capturing.
The usual notion of composition of formulas can be extended to -systems as follows.
Let S be a -system. The scope of a left variable y in S is the set of all variables z such that there is a LEF T path from y to z.
Let S; T be two systems where the variables at left of S and T are disjoint. Let A be an atom of S. Then the composition of S and T is the system obtained by concatenating the equations of S and of T and by replacing A with the left variable of the rst equation of T . Composition is possible only without capture, i.e. T must not have free variables y such that some occurrence of A is in the scope of y in S. 2.6
We de ne the vectorial hierarchies V EC n, V EC n, V EC n as follows. V EC 0 = V EC 0 are the modal systems. V EC n+1 is the closure of V EC n under composition and adding a equation as a rst equation of the system. V EC n+1 is the closure of V EC n under composition and adding a equation as a rst equation of the system. V EC n = V EC n\V EC n. The alternation depth of a system S is the least n such that S is in V EC n+1. 3 3.1
Like it is usually done for modal logic, we give Kripke semantics to the -calculus by using the notion of model.
A graph (also called frame) is a pair G = (V; E), where V is a set of vertices and E is a binary edge relation on V .
A graph G = (V; E) is called total if E = V 2, i.e., all possible edges are present.
A path in a graph G from a vertex x to a vertex y is a nite sequence of vertices z1; : : : ; zn such that z1 = x, zn = y and ziEzi+1 for every i < n.
A point y is reachable from a point x if there is a path from x to y.
A model is a pair (G; Col), where G is a graph and Col is a coloring function from some domain D to the powerset of V . 3.2
Intuitively, bisimulation between models indicates that the two models have the same observable behavior. Formally, we can de ne a bisimulation between two models (G; Col) and (G0; Col0) as a relation B V (G) V (G0) such that, whenever (xBx0): { x 2 Col(d) if and only if x0 2 Col0(d) for every d 2 D; { if xEy, then there is y0 such that x0E0y0 and yBy0; { if x0E0y0, then there is y such that xEy and yBy0.
We say that two pointed colored graphs (G; Col; x) and (G0; Col0; x0) are bisimilar if and only if there is a bisimulation B such that xBx0. 3.3
We consider a few subclasses of graphs.
A graph (V; E) is called total if E = V 2, that is, all possible edges are present.
The class K4 is the class of all (vertex colored) graphs whose relation is transitive. The class S5 is the class of all (vertex colored) graphs whose relation is an equivalence relation. Since equivalence relations are re exive, symmetric and transitive, S5 is included in K4 (as a class of graphs). The names K4 and S5 come from the modal logic literature.
We also speak of total models, K4 models and S5 models in the obvious sense.
Note that every total graph belongs to S5. Moreover, for every S5 model M and every vertex x of M , there is a total model M 0 containing x such that (M; x) and (M 0; x) are bisimilar: in fact M 0 is the submodel of M given by all points of M reachable from x.
Moreover, every S5 model M is bisimilar to a S5 graph M 0, colored in the same way, where every two di erent points have di erent colors: in fact, M 0 is M modulo the equivalence relation of having the same color, and the bisimulation is the projection function. 3.4
The semantics of -calculus extends the usual Kripke semantics for modal logic. So, to give semantics to the -calculus, we must consider models of the form M = (G; V al) where G = (V; E) is a graph and V al is a valuation function from At [ V ar to the powerset of V . To each model M and each formula we can associate a subset jj jjM of V , de ned in this way: { jjAjjM = V al(A) and jj:AjjM = V n V al(A) if A is an atom; { jjXjjM = V al(X); { jj _ jjM = jj jjM [ jj jjM ; { jj ^ jjM = jj jjM \ jj jjM ; { jjh i jjM is the set of all elements of V having some successor in jj jjM ; { jj[ ] jjM is the set of all elements of V having every successor in jj jjM ; { jj X: (X)jjM is the smallest set S V such that S = jj jjM [X := S], where M [X := S] is obtained from M by letting V al(X) = S; { jj X: (X)jjM is the greatest set S V such that S = jj jjM [X := S]. The last two items are well de ned since the map sending S to jj jjM [X := S] is a monotonic function on the powerset of V and so, by the Knaster-Tarski Theorem, this map has both a least and a greatest xpoint.
We also say that a vertex v of a model M veri es a formula , written M; v j= , if v 2 jj jjM . 4 4.1
It is notoriously di cult to understand -calculus formulas, especially when there are many alternating xpoints. A means to understand the -calculus is given by parity games. We will see that the semantics of -calculus formulas can be given in terms of parity games.
Intuitively, a parity game is a game where two players, called c and d, move in a graph (the notation, due to Arnold, suggests that c means conjunctive and d means disjunctive). The vertexes of the graph are labeled with nitely many positive integers. d wants to have many high even numbers along the play, whereas c wants to have many odd numbers.
Let us de ne parity games more formally. A parity game is a structure = (Vc; Vd; E; v0; ), where Vc and Vd are disjoint sets, E is a binary relation on Vc [ Vd, v0 2 Vc [ Vd is the initial vertex, and : Vc [ Vd ! f1; : : : ; ng is the priority function; the number n is called the index of the game.
A play of is a sequence of vertices, starting from v0, where the successor of the current vertex must be an E-successor of that vertex, and this successor is chosen by the player d, if the vertex is in Vd, and by c if the vertex is in Vc.
If the play reaches a position where either player has no moves, the other wins. If this never happens, then the play is in nite, and d wins if the greatest priority occurring in nitely often is even, and c wins otherwise.
A strategy of a player p is a function which, given an initial segment of a play ending with a p- position, determines the next move of p. A strategy is positional if the move depends only on the last vertex of the segment.
A strategy of a player p is winning if every play where p moves according to is won by p.
Note that parity games are Borel games, so by Borel determinacy, see [
A well known property of parity games is positional determinacy:
Theorem 1. (See [
However in this paper we will use a slightly stronger form of determinacy. Let us call a strategy strongly positional if the move on a position depends only on the successors of the position (not on the position itself). Clearly, a strongly positional strategy is positional, but the converse does not hold: if two di erent nodes have the same successors, a stronlgy positional strategy gives the same answer on the two nodes, whereas a positional one need not to.
Now a careful analysis of [
Proof. Note that players c and d are called AN D and OR in [
The semantics of the -calculus can be given in terms of a parity game. More precisely, given a sentence and a model M = (V; E; V al), with a distinguished vertex v0 of V , we can de ne an evaluation game ( ; v0; M ) as follows (we consider sentences rather than arbitrary formulas for simplicity).
The positions of ( ; v0; M ) are the pairs ( ; v), where v 2 V and is a subformula of . The d positions are the pairs of the form ( _ ; v) or (h i ; v); all other positions are c positions. ( ; v0) is the initial position.
There are edges from ( _ ; v) or ( ^ ; v) to ( ; v) and ( ; v); from (h i ; v) or ([ ] ; v) to ( ; w) for every successor w of v in V ; from ( X: ; v) and ( X: ; v) to ( ; v); and if a variable occurrence X appears in a subformula X: or X: , there is an edge from (X; v) to ( X: ; v) or ( X: ; v) respectively. Finally, we put also an edge from (A; v) or (:A; v) to itself for every atom A, and from (Y; v) to itself for every variable Y free in .
To de ne the function we proceed as follows. First we assign priorities to xpoint subformulas of : we assign to each greatest xpoint subformula X: in a priority 2j j, and we assign to X: a priority 2j j + 1. This ensures that: { least xpoints have odd priority; { greatest xpoints have even priority; { the priority of larger subformulas is larger.
Now we let ( ; v) be the priority of , if is a xpoint formula; (A; v) = 2 if M; v j= A and (A; v) = 1 otherwise, if A is an atom, a negated atom or a free variable of ; and ( ; v) = 1 otherwise.
It results that M; v0 j= if and only if player d has a winning strategy in ( ; v0; M ). 4.3
We have seen that in a sense, -calculus reduces to parity games. However, as is well known, also the other way round is true: if we consider parity game of index n as a graph vertex-colored by c; d; 1; : : : ; n, then there is a -calculus formula Wn, due to Walukiewicz, such that an arena for parity games (G; v0) veri es Wn if and only if player d has a winning strategy in the parity game associated to (G; v0). This formula is
Wn =
X1 X2 : : : Xn:(d ! h i ^(i ! Xi) ^ (c ! [ ] ^(i ! Xi): i i 5
In [
Proof. Let M = (V; E; V al) be a model. Let S be a modal -system. Up to perform a polynomial time rewriting of S, we can suppose that the equations of S have one of the following forms: X = A, X = :A where A is an atom, X = Y _ Z, X = Y ^ Z, X = h iY , X = [ ]Y , X = Y .
Now M 0 is obtained as follows. The vertices of M 0 are the vertices of M . Let us enumerate these vertices as v1; : : : ; vn. Let Ai be an atom which is true in G' only in the point vi. The relation E0 of M 0 holds for every pair of vertices of M 0, so M 0 is an S5 model.
Moreover S0 is obtained by replacing every equation of S of the form
X = ^fAi ! h i(Aj ^ Y )jviRvj g:
Note that one could expect that the right hand side of X = [ ]Y is replaced by the De Morgan dual of X = h iY , so to have VfAi ! [ ](Aj ! Y )jviRvj g. However, the atoms Ai are interpreted as singletons, so
X = _fAi ^ h i(Aj ^ Y )jviRvj g;
X = h iY
X = [ ]Y [ ](Aj ! Y ) with with and every equation of S of the form is in fact equivalent to its De Morgan dual
h i(Aj ^ Y ); and this allows us to replace the box with the diamond.
We do not know whether Theorem 2 can be specialized to the scalar calculus. In fact, the problem is that the translation from a modal -system to a single formula of the modal -calculus (i.e., the algorithm which builds the solution of a modal -system) takes exponential time in general. 6
It is well known that there is a translation of vectorial -calculus in S5 to vectorial modal logic in S5. In fact, given a modal -system in S5, we can rst consider its solution and translate it into modal logic. From the previous theorem we obtain: Corollary 2. If there is a polynomial time computable translation from boxfree vectorial -calculus in S5 to vectorial modal logic in S5, then the vectorial -calculus model checking problem is in P .
Proof. By [
Considerations analogous to S5 hold in the larger class of graphs K4. In fact,
from [
Proof. Every S5 graph is also a K4 graph, so by the previous theorem, there
is a polynomial time reduction from vectorial model checking over arbitrary
graphs to vectorial model checking in K4. Moreover, by [
In this section we investigate the -calculus satis ability problem for S5. We begin with establishing a linear size model property.
Proof. Let (M; x0) be a S5 model of . Up to bisimulation we can suppose that M is total. Then player d has a winning strategy in the game ( ; x0; M ). By Corollary 1, d has a strongly positional winning strategy in the game, call it . Consider a diamond position (h i ; y) of the game. Since M is total, the set of successors of (h i ; y) does not depend on y, so the choice of also does not depend on y, but only on . Let us denote by ( ; x ) the successor position of (h i ; y) chosen by . Let N be the submodel of M given by x0 plus all points x .
First, N has size linear in because its size is at most the number of diamond subformulas of (plus one). Moreover, we note that if player c in the game always chooses elements of N in box positions, then the game remains in N forever, and is won by d since is winning on M . tu Theorem 3. The satis ability problem for the -calculus in S5 is N P -complete. Proof. N P -hardness holds because the -calculus contains propositional logic.
To show that the problem is in N P , suppose that models and formulas are encoded as strings in a convenient nite alphabet (e.g. ASCII code). We prove that there is a problem S in P T IM E and a polynomial p such that is satis able in S5 i there exists a witness z such that ( ; z) 2 S and length(z) p(length( )).
Since -calculus model checking is in N P (see [
Let S be the set of tuples ( ; M; y) such that: { M is an S5 model (i.e. the accessibility relation is an equivalence); { (M; ; y) 2 S0; { length(M ) r(length( )); { length(y) q(length(M ) + length( )).
So, is satis able in S5 if and only if there exists a witness z = (M; y) such that ( ; z) 2 S. Note that S is in P T IM E. Moreover, ( ; z) 2 S implies length(z) p(length( )), where p(x) = r(x) + q(r(x) + x). So, is satis able in S5 if and only if there exists a witness z = (M; y) such that ( ; z) 2 S and length(z) p(length( )). So S and p satisfy the desired properties.
Note that the restriction of the previous theorem to modal logic was already
known, see [
A formula of the -calculus is called existential, or box-free, if it contains no
box operators [ ] . Intuitively, existential -calculus is considerably simpler
than general -calculus. In fact, the satis ability problem for the -calculus
is EXP T IM E-complete, whereas, as shown in [
First we observe: Lemma 2. The satis ability problem for existential -calculus is polynomial time equivalent to the same problem on S5.
Proof. If an existential formula has a model M , then is also true on the re exive, symmetric, transitive closure of M , which is an S5 graph of the same size as M .
Moreover, as a corollary of the previous section we have: Corollary 4. The satis ability problem for existential -calculus in S5 is N P complete.
Proof. The satis ability problem for existential -calculus in S5 is N P because, by Theorem 3, it is a particular case of an N P problem. Moreover, the problem is N P -hard because existential -calculus contains propositional logic.
From the previous lemma and the previous corollary it follows: Corollary 5. The satis ability problem for existential -calculus is N P -complete. tu tu 9
On
-calculus and modal logic in S5 It is known that -calculus in S5 is as expressive as modal logic, so in S5 there is no xpoint alternation hierarchy. In this section we describe two translations from -calculus to modal logic; the rst is due to Alberucci and Facchini, whereas the second is based on a bisimulation argument. 9.1
In [
A -calculus sentence is well named if it is guarded and, for any variable X, no two distinct occurrences of xpoint operators in bind X, and the atom X occurs only once in .
Using the semantical laws X: (X; X) = X: Y: (X; Y ), X: (X; X) =
X: Y: (X; Y ) (see [
The following translation t from well named -formulas to modal logic in S5 can be de ned: { t(A) = A; t(:A) = :A; { t(true) = true, t(f alse) = f alse; { t(h i ) = h it( ); { t([ ] ) = [ ]t( ); { t( ^ ) = t( ) ^ t( ); { t( _ ) = t( ) _ t( ); { t( X: (X)) = t(( ( (f alse)) ); { t( X: (X)) = t(( ( (true)) ), where ( ( (f alse)) ; ( ( (true)) denote the well named formulas obtained from ( (f alse)); ( (true)) by renaming repeated bound variables. The translation t is given by induction on the rank, so it is well de ned. Moreover:
is a well named formula, then the length of t( ) is at most 2j j.
Proof. We need a preliminary composition lemma: Lemma 4. t( [X= ]) = t( )[X=t( )].
Proof. By induction on .
Now the bound as in the lemma can be proved by induction on the rank of . The most delicate case is X: (X) and X: (X). Now, by Lemma 4, we have t( X: (X)) = t( ( (f alse)) = t( )[X=t( (f alse))], and since X occurs only once in , we obtain the bound jt( X: )j = jt( )[X=t( (f alse))]j 2jt( (f alse))j 2 2j (false)j = 2j (false)j+1 2j X: (X)j. The case of is analogous.
So, the translation t is at most exponential. We also can show that the exponential upper bound for the translation t is tight. In fact, consider the well named formulas: n =
X1 : : : Xn:X1 _ (X2 _ : : : _ Xn): We can show by induction that t( n) has size at least 2n. In fact, the base case n = 1 is true; for the inductive case, we begin with a lemma: tu tu
{ jt( (f alse _ ))j > jt( ( )j; { if X is a variable free in , then jt( (X _ ))j > jt( ( )j.
Now consider t( n) with n > 1. By de nition of t we have
t( n) = t( X2 : : : Xn:( X2 : : : Xn:f alse _ X2 _ : : : _ Xn) _ X2 : : : _ Xn) and by Lemma 4 we obtain t( n) = t( X2 : : : Xn:Y _ X2 : : : _ Xn)[Y =t( X2 : : : Xn:f alse _ X2 _ : : : _ Xn): By evaluating the sizes we see that jt( n)j jt( X2 : : : Xn:Y _X2 : : :_Xn)j+jt( X2 : : : Xn:f alse_X2_: : :_Xn)]j 1; tu by Lemma 5 we obtain and, by renaming the variables, jt( n)j 2jt( X2 : : : Xn:X2 _ : : : Xn)j; jt( n)j
2jt( n 1)j: Finally, the inductive hypothesis gives jt( n 1)j 2n 1, so jt( n)j 2n. 9.2
A translation from -calculus to modal logic di erent from [
Both translations of the previous subsections give an exponential blow up in the size of the formula. It is then natural to ask whether there exists a polynomial time computable translation from the -calculus to modal logic over S5. This question is related to the results of the previous section, as the following nal corollary shows: Corollary 6. If there is a polynomial time computable translation from the calculus to modal logic over S5 and Theorem 2 specializes to scalar -calculus, then the -calculus model checking problem is in P .
Proof. Given a -formula and a model M , rst reduce the problem to a formula 0 over an S5 model M 0, and then apply the polynomial translation in order to obtain a modal formula with
M j= , M 0 j= : Since both M 0 and are obtained in polynomial time from M; model checking is in P , we have done. and modal tu 10
In this paper we have investigated some aspects of -calculus on S5 graphs. Arguably, these graphs are quite simple. However, simplicity of S5 graphs gives us better satis ability bounds than arbitrary graphs, but not better bounds on the model checking problem.
An interesting question is whether there is a direct, natural translation from modal systems to modal systems in S5: by this we mean that the translation should not go through transforming a system of equations into a single scalar term.
A similar analysis of -calculus model checking and satis ability could be carried over other important classes of graphs. An example is K4. Since satis ability in K4 e ciently reduces to general satis ability, in K4 we have the same bound as in K, that is, EXP T IM E. It would be interesting to see whether a better bound can be given. Note that for model checking, as we have seen, a better bound for K4 with respect to arbitrary graphs does not exist.
The same analysis could be done for other interesting classes of graphs, e.g.
the longstanding Godel-Lob class GL (i.e. the transitive wellfounded graphs),
or for more recent classes such as graphs of bounded tree width or classes with
forbidden minors. A good model checking algorithm for bounded tree width is
e.g. [
This work has been partially supported by the PRIN project n. 20089M932N Innovative and multi-disciplinary approaches for constraint and preference reasoning.