EstiMate is an approximate model counter, designed to estimate the number of models for a given LTL formula. It utilizes a transfer matrix, generated through a series of tree encodings, to provide approximate model counts.
If you utilize EstiMate for research purposes, we kindly request that you cite the corresponding paper where the technique was introduced and evaluated: Automated Repair of Unrealisable LTL Specifications Guided by Model Counting. Thank you :)
@inproceedings{10.1145/3583131.3590454,
author = {Brizzio, Mat\'{\i}as and Cordy, Maxime and Papadakis, Mike and S\'{a}nchez, C\'{e}sar and Aguirre, Nazareno and Degiovanni, Renzo},
title = {Automated Repair of Unrealisable LTL Specifications Guided by Model Counting},
year = {2023},
isbn = {9798400701191},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3583131.3590454},
doi = {10.1145/3583131.3590454},
booktitle = {Proceedings of the Genetic and Evolutionary Computation Conference},
pages = {1499–1507},
numpages = {9},
keywords = {search-based software engineering, LTL-synthesis, model counting},
location = {Lisbon, Portugal},
series = {GECCO '23}
}
This code is implemented and maintained by Matias Brizzio and Renzo Degiovanni
The transfer matrix, denoted as Tϕ, is generated using the following steps:
- Generate the Buchi automaton Bϕ that recognizes the specification ϕ.
- From Bϕ, generate a Finite State Automaton Aϕ.
- Generate the transfer matrix Tϕ from Aϕ.
The Buchi automaton Bϕ recognizes lasso traces satisfying the formula ϕ. A lasso trace is an infinite trace that loops back to a previous state, forming a cycle. It accepts infinite traces, as its accepting condition requires visiting an accepting state infinitely often in the lasso trace. In contrast, finite automata recognize finite traces, as their accepting condition only requires reaching a final state.
When generating the finite automaton Aϕ from Bϕ, the finite traces recognized by Aϕ become part of the lasso traces recognized by Bϕ.
The finite automaton Aϕ is encoded into an N x N transfer matrix Tϕ, where N represents the number of states in Aϕ. Each element Tϕ[i,j] in the matrix denotes the number of transitions from state i to state j.
By using matrix multiplication, the number of traces of length k accepted by Aϕ can be computed as I x Tϕk x F. Here, I is a row vector representing the initial states, Tϕk is the matrix resulting from multiplying Tϕ k times, and F is a column vector representing the final states of Aϕ.
Linear Temporal Logic (LTL) 🕰️
The grammar for LTL aims to support Spot-style LTL. For further details on temporal logic, e.g., semantics, see here.
- True:
tt
,true
,1
- False:
ff
,false
,0
- Atom:
[a-zA-Z_][a-zA-Z_0-9]*
or quoted"[^"]+"
- Negation:
!
,NOT
- Implication:
->
,=>
,IMP
- Bi-implication:
<->
,<=>
,BIIMP
- Exclusive Disjunction:
^
,XOR
- Conjunction:
&&
,&
,AND
- Disjunction:
||
,|
,OR
- Parenthesis:
(
,)
- Finally:
F
- Globally:
G
- Next:
X
- (Strong) Until:
U
- Weak Until:
W
- (Weak) Release:
R
- Strong Release:
M
To ensure the accurate interpretation of provided LTL formulas, the parser adheres to the following precedence rules:
-
Binary Expressions: These expressions involve two operands and an operator. Examples include conjunction (
&&
,&
,AND
), disjunction (||
,|
,OR
), implication (->
,=>
,IMP
), bi-implication (<->
,<=>
,BIIMP
), exclusive disjunction (^
,XOR
), strong until (U
), weak until (W
), weak release (R
), and strong release (M
). -
Unary Expressions: These expressions involve a single operand and an operator. Examples include negation (
!
,NOT
), next (X
), globally (G
), and finally (F
). -
Literals, Constants, Parentheses: These are fundamental components of the formula. Literals represent atomic propositions, constants denote truth values (e.g.,
tt
for true,ff
for false), and parentheses are used to group subexpressions.
The precedence hierarchy is structured as follows:
OR
< AND
< Binary Expressions
< Unary Expressions
< Literals
, Constants
, Parentheses
This means that binary expressions take precedence over unary expressions, which, in turn, take precedence over literals, constants, and parentheses. For instance, in the expression a && b || c
, the conjunction (&&
) is evaluated before the disjunction (||
), and parentheses can be employed to override this precedence.
Moreover, for chained binary expressions lacking parentheses, the rightmost binary operator holds precedence. For example, a -> b U c
is parsed as a -> (b U c)
.
- Java 18 or later.
To compile Estimate just run the following bash command.
make compile
Additionally, if you desire to get jar file together with the compilation run
make
This last rule will not only compile the whole project but also create a jar file (into the dist
folder) you can use inside your projects.
The tool can take as input either a specification in TLSF format or directly an LTL formulae. To run, you have to use the script modelcount.sh
.
./modelcount.sh case-studies/arbiter/arbiter.tlsf
or:
./modelcount.sh -formula="(F (a && p))" -k=10 -vars=a,p [-flags] [-to=timeout]
-auto = enables EstiMate
-re = uses a Regular expression model counter
without flag; uses exact model counter
This README is here to give you a complete rundown of EstiMate, covering its features and how to use it effectively. If you have any questions or come across any roadblocks, don't hesitate to get in touch with us.
Thanks for taking an interest in EstiMate! 🦉
Happy coding and may your projects soar to new heights! 🚀
EstiMate has recently been employed to resolve conflicts within complex real-world LTL specifications [1]. Additionally, it has been utilized to detect bugs in some of the most commonly used SAT solvers [2] within the SE and formal methods communities