Manual

User Manual: Pdf

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

Download
Open PDF In Browser	View PDF

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 S is 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 certificate. Jatatosk expects all
parts as input, i. e., a file 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

Defining the Vocabulary

The first thing that has to be defined 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 first input line must be of the following
form:
vocabulary R1 ar(R1 ) R2 ar(R2 ) . . . Rr ar(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

2

vocabulary E 2 R 1 G 1

vocabulary E 2 R 2

Specifying the Structure

Once the vocabulary is defined, 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 defines that the universe of the structure is U = {0, 1, . . . , n − 1} and that exactly m lines follow that
define the interpretation of the Ri in the structure. Assume we wish to define the structures
,
, and
over the vocabularies of the previous section, then we may achieve this as follows:
structure 4 5
E 0 1
E 0 2
E 1 2
E 1 3
E 2 3

structure 4 9
E 0 1
E 0 2
E 1 2
E 1 3
E 2 3
R 0
R 3
G 1
G 2
1

structure 4 6
E 0 1
E 0 2
E 1 2
E 1 3
E 2 3
R 0 3

Observe that E is automatically interpreted symmetrically, i. e., the graph will always be undirected. In contrast,
the other relations that we have specified (as the binary relation R in 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 define first. All formulas ϕ must be of the form:
ϕ = Q1 X1 Q2 X2 . . . Qq Xq

`
^

ψi ,

i=1

where the Qj are second-order quantifiers to be defined in a second, the Xj are monadic second-order variables,
and the ψi are first-order formulas to be defined in a minute. There are three existential quantifiers available:
Qj ∈ { ∃partition , ∃connected , ∃forest }. The partition quantifier ∃partition P1 , P2 , . . . , Pk quantifiers over partitions
of the universe (into k partitions). Note that we can express a “classical” existential quantifier simply as
∃X ≡ ∃partition X, X̄. The connected quantifier ∃connected C quantifies over subsets of the universe that are
connected with respect to the relation E (in graph theoretic terms), i. e., it quantifies over connected subgraphs.
Finally, the forest quantifier ∃forest F quantifies over subsets of the universe that are acyclic with respect to E
(in graph theoretic terms), i. e., it quantifies over subgraphs that are forests. To specify these quantifiers in the
input, we add one line per quantifier 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 quantifier that guesses a connected set C; and a quantifier that guesses a forest F .
exists R G B

connected C

forest F

The first-order formulas ψi have 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 χi are quantifier free first-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 p is an integer that indicates the number of clauses of χi (which are defined in
the following p lines).
Formula

Input

∀x∀y E(x, y) → χi (x, y)
∀x∃y E(x, y) ∧ χi (x, y)
∃x∀y E(x, y) → χi (x, y)
∃x∃y E(x, y) ∧ χi (x, y)
∀x χi (x)
∃x χi (x)

axay p
axey p
exay p
exey p
ax p
ex p

After a ψi was introduced as defined in the table, the following p lines each define one clause of χi . Every
clause is presented by a space-separated line that contains a relation symbol R (either a quantified second-order
variable, a free second-order variable, or a relation of the structure), followed by ar(R) first-order variables (x
and y) or elements of the universe. In particular, a clause may defined as follows:
R x1 x2 . . . xar(R) R̃ x̃1 x̃2 . . . x̃ar(R̃) . . .
Additionally, we may negate relational symbols by adding a minus-sign (“-”) in front of it (−R). Furthermore,
we may have that R is “=”, which is a special symbol that is directly build into the logic. As one might expect,
“=” is of arity 2 and 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)) , ∀x R(x) → C(x) , and
∃x∀y E(x, y) → R(x, y) over the three vocabularies of the previous sections as follows:
axay
-R x
-G x
-B x

3
-R y
-G y
-B y

ax 1
-R x C x

exay 1
R x y

2

4

Free Variables and Optimization Problems

Jatatosk may also be used to solve optimization problems, which are usually not captured by classical modelchecking. To express an optimization problem, we consider formulas ϕ(X1 , . . . , Xk ) with free monadic secondorder variables X1 , . . . , Xk , and
Pkweight
P functions ω1 , . . . , ωk with ωi : U → Z. Jatatosk can now find sets
S1 , . . . , Sk ⊆ U that minimize i=1 s∈Si ωi (si ) with respect to S |= ϕ(S1 , . . . , Sk ). To define a free variable,
we present a line to Jatatosk that starts with min, followed by the name of the variable, followed by n integers
that define the weights for the universe. For instance, the following examples add free variables X, Y , and Z
with weight functions x 7→ 1, x 7→ x, and x 7→ x2 , respectively.
min X 1 1 1 1

5

min Y 0 1 2 3

min Z 0 1 4 9

Comments and Restrictions

To increase the readability of structures and formulas that are stored in a file, 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
E 0 1
E 0 2
c
c We may also comment parts of the structure.
c
E 1 2
E 1 3
E 2 3
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 defined, 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 file. A comment-line in the input
mentions the problem defined by the formula.

∃partition R, G, B

^



∀x∀y E(x, y) → ¬C(x) ∨ ¬C(y)

C ∈ {R, G, B}



ϕ(S) = ∀x∀y E(x, y) → S(x) ∨ S(y)

4

c
c Solve 3-coloring.
c
vocabulary E 2
structure 4 5
E 0 1
E 0 2
E 1 2
E 1 3
E 2 3
exists R G B
axay 3
-R x -R y
-G x -G y
-B x -B y
c
c Compute a
c minimum
c vertex-cover.
c
vocabulary E 2
structure 6 7
E 0 1
E 0 2
E 1 2
E 1 3
E 3 4
E 3 5
E 4 5
min S 1 1 1 1 1 1 1
axay 1
S x S y



∃connected A ∃connected B ∀x R(x) → A(x)


∧ G(x) → B(x)


∧ ¬A(x) ∨ ¬B(x)

ϕ(S) = ∃forest F ∀x S(x) ∨ F (x)




References
[1] J. Flum and M. Grohe. Parameterized Complexity Theory. Springer, 2006.
[2] N. Immerman. Descriptive Complexity. Springer, 1999.

5

c
c Find disjoint
c paths between
c red and green
c vertices.
c
vocabulary E 2 R 1 G 1
structure 9 17
E 0 1
E 0 3
E 1 4
E 1 2
E 2 5
E 3 4
E 3 6
E 4 5
E 4 7
E 5 8
E 6 7
E 7 8
E 3 5
R 2
R 6
G 0
G 8
connected A
connected B
ax 4
-R x A x
-G x B x
-A x -B x
c
c Compute a minimum
c feedback-vertex
c set.
c
vocabulary E 2
structure 5 6
E 0 1
E 0 2
E 0 3
E 0 4
E 2 3
E 3 4
min S 1 1 1 1 1
forest F
ax 1
S x F x



---

Source Exif Data:

File Type                       : PDF
File Type Extension             : pdf
MIME Type                       : application/pdf
PDF Version                     : 1.5
Linearized                      : No
Page Count                      : 5
Producer                        : LuaTeX-1.0.4
Creator                         : TeX
Create Date                     : 2018:04:23 23:41:02+02:00
Modify Date                     : 2018:04:23 23:41:02+02:00
Trapped                         : False
PTEX Full Banner                : This is LuaTeX, Version 1.0.4 (TeX Live 2017)

EXIF Metadata provided by EXIF.tools