Manual

User Manual: Pdf

Open the PDF directly: View PDF PDF.
Page Count: 5

Jatatosk: A Lightweight Model-Checker for a Small Fragment of MSO
Max Bannach
April 23, 2018
We describe the usage of the lightweight monadic second-order model-checker Jatatosk. A model-checker is a
tool that, given a vocabulary (or signature)τ, a logical τ-structure S, and a τ-formula ϕof some logic, decides
whether or not S |=ϕholds. In the case that Sis a model of ϕ, the model-checker is also required to output an
assignment of the free and existential-bounded second-order variables of ϕas a certicate. Jatatosk expects all
parts as input, i. e., a le containing a signature, a structure, and a formula. This documents explains how these
objects have to be presented to Jatatosk, and which restrictions we postulate for the signature, the structure,
and the formula. It does, however, not serve as an introduction to logic and we refer the interested reader to
the standard textbooks, for instance [2, 1].
1 Dening the Vocabulary
The rst thing that has to be dened is the vocabulary τ= (R1, R2, . . . , Rr), which may only contain relational
symbols of arity ar(Ri). In particular, we do not allow function symbols or constants. Furthermore, τmust
contain a binary relation E. To present the vocabulary to Jatatosk, the rst input line must be of the following
form:
vocabulary R1ar(R1)R2ar(R2). . . Rrar(Rr)
The following examples show from left to right: a vocabulary for graphs; for graphs in which vertices may be
colored red or green; and graphs in which we have additional (directed) red edges.
vocabulary E 2 vocabulary E 2 R 1 G 1 vocabulary E 2 R 2
2 Specifying the Structure
Once the vocabulary is dened, the next thing to do is to specify the actual structure on which we work. As
mentioned in the previous section, the structure must contain the binary relation E, and we further stipulate
that the structure must interpret this relation in a symmetric fashion. In other words, the structure must
contain an undirected graph as substructure. To present the structure to Jatatosk, the second input-line must
have the following form:
structure n m
This denes that the universe of the structure is U={0,1, . . . , n −1}and that exactly mlines follow that
dene the interpretation of the Riin the structure. Assume we wish to dene the structures , , and
over the vocabularies of the previous section, then we may achieve this as follows:
structure 4 5
E01
E02
E12
E13
E23
structure 4 9
E01
E02
E12
E13
E23
R 0
R 3
G 1
G 2
structure 4 6
E01
E02
E12
E13
E23
R03
1
Observe that Eis automatically interpreted symmetrically, i. e., the graph will always be undirected. In contrast,
the other relations that we have specied (as the binary relation Rin the third example) are not symmetric.
3 Adding a Formula
The last ingredient we need is the formula. Jatatosk works on a small fragment of monadic second-order logic,
which we shall dene rst. All formulas ϕmust be of the form:
ϕ=Q1X1Q2X2. . . QqXq
`
^
i=1
ψi,
where the Qjare second-order quantiers to be dened in a second, the Xjare monadic second-order variables,
and the ψiare rst-order formulas to be dened in a minute. There are three existential quantiers available:
Qj∈ { ∃partition,∃connected,∃forest }. The partition quantier ∃partitionP1, P2, . . . , Pkquantiers over partitions
of the universe (into kpartitions). Note that we can express a “classical” existential quantier simply as
∃X≡ ∃partitionX, ¯
X. The connected quantier ∃connectedCquanties over subsets of the universe that are
connected with respect to the relation E(in graph theoretic terms), i. e., it quanties over connected subgraphs.
Finally, the forest quantier ∃forestFquanties over subsets of the universe that are acyclic with respect to E
(in graph theoretic terms), i. e., it quanties over subgraphs that are forests. To specify these quantiers in the
input, we add one line per quantier that starts with the name (exists,connected,forest), followed by
a list of bounded variables. For instance, the following examples show: a partition of the universe into R,G,
B, i. e., a 3-coloring; a quantier that guesses a connected set C; and a quantier that guesses a forest F.
exists R G B connected C forest F
The rst-order formulas ψihave to be of a very restricted form as well. In particular, only formulas of the
form presented in the left side of the following table are allowed. Here, the χiare quantier free rst-order
formulas in canonical normal form. The right side of the table describes the syntax that is used to present such
a formula to Jatatosk, where the pis an integer that indicates the number of clauses of χi(which are dened in
the following plines).
Formula Input
∀x∀y E(x, y)→χi(x, y)axay p
∀x∃y E(x, y)∧χi(x, y)axey p
∃x∀y E(x, y)→χi(x, y)exay p
∃x∃y E(x, y)∧χi(x, y)exey p
∀x χi(x)ax p
∃x χi(x)ex p
After a ψiwas introduced as dened in the table, the following plines each dene one clause of χi. Every
clause is presented by a space-separated line that contains a relation symbol R(either a quantied second-order
variable, a free second-order variable, or a relation of the structure), followed by ar(R)rst-order variables (x
and y) or elements of the universe. In particular, a clause may dened as follows:
R x1x2. . . xar(R)˜
R˜x1˜x2. . . ˜xar(˜
R). . .
Additionally, we may negate relational symbols by adding a minus-sign (“-”) in front of it (−R). Furthermore,
we may have that Ris “=”, which is a special symbol that is directly build into the logic. As one might expect,
“=” is of arity 2and does exactly evaluate to true for equal elements. We can express the following three
formulas ∀x∀y E(x, y)→¬R(x)∨ ¬R(y)) ∧(¬G(x)∨ ¬G(y)) ∧(¬B(x)∨ ¬B(y)),∀xR(x)→C(x), and
∃x∀y E(x, y)→R(x, y)over the three vocabularies of the previous sections as follows:
axay 3
-R x -R y
-G x -G y
-B x -B y
ax 1
-RxCx
exay 1
Rxy
2
4 Free Variables and Optimization Problems
Jatatosk may also be used to solve optimization problems, which are usually not captured by classical model-
checking. To express an optimization problem, we consider formulas ϕ(X1, . . . , Xk)with free monadic second-
order variables X1, . . . , Xk, and weight functions ω1, . . . , ωkwith ωi:U→Z.Jatatosk can now nd sets
S1, . . . , Sk⊆Uthat minimize Pk
i=1 Ps∈Siωi(si)with respect to S |=ϕ(S1, . . . , Sk). To dene a free variable,
we present a line to Jatatosk that starts with min, followed by the name of the variable, followed by nintegers
that dene the weights for the universe. For instance, the following examples add free variables X,Y, and Z
with weight functions x7→ 1,x7→ x, and x7→ x2, respectively.
minX1111 minY0123 minZ0149
5 Comments and Restrictions
To increase the readability of structures and formulas that are stored in a le, we may add at any point a
comment-line, which is indicated with a leading c.
c We may add a comment before we even start!
c
vocabulary E 2
c A comment between the vocabulary and the structure.
structure 4 5
E01
E02
c
c We may also comment parts of the structure.
c
E12
E13
E23
axay 3
-R x -R y
c Or we may add a comment to the formulas.
-G x -G y
-B x -B y
To make the input format well dened, we forbid that any relational symbol of the vocabulary, any free variable,
and any bounded variable has the name “c”, “=”, or a name that starts with “-”.
3
6 Examples
We illustrate the full input format with some complete examples. In the following overview, on the left we show
a structure, in the center a formula, and at the right the corresponding input le. A comment-line in the input
mentions the problem dened by the formula.
∃partitionR, G, B ^
C∈ {R, G, B}
∀x∀y E(x, y)→¬C(x)∨ ¬C(y)
c
c Solve 3-coloring.
c
vocabulary E 2
structure 4 5
E01
E02
E12
E13
E23
exists R G B
axay 3
-R x -R y
-G x -G y
-B x -B y
ϕ(S) = ∀x∀y E(x, y)→S(x)∨S(y)
c
c Compute a
c minimum
c vertex-cover.
c
vocabulary E 2
structure 6 7
E01
E02
E12
E13
E34
E35
E45
minS1111111
axay 1
SxSy
4
∃connectedA∃connectedB∀xR(x)→A(x)
∧G(x)→B(x)
∧¬A(x)∨ ¬B(x)
c
c Find disjoint
c paths between
c red and green
c vertices.
c
vocabulary E 2 R 1 G 1
structure 9 17
E01
E03
E14
E12
E25
E34
E36
E45
E47
E58
E67
E78
E35
R 2
R 6
G 0
G 8
connected A
connected B
ax 4
-RxAx
-GxBx
-A x -B x
ϕ(S) = ∃forestF∀xS(x)∨F(x)
c
c Compute a minimum
c feedback-vertex
c set.
c
vocabulary E 2
structure 5 6
E01
E02
E03
E04
E23
E34
minS11111
forest F
ax 1
SxFx
References
[1] J. Flum and M. Grohe. Parameterized Complexity Theory. Springer, 2006.
[2] N. Immerman. Descriptive Complexity. Springer, 1999.
5

Navigation menu