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)
.
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! ๐