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.,
ttfor true,fffor 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 compileAdditionally, if you desire to get jar file together with the compilation run
makeThis 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 counterwithout 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, this idea was used in [2] to measure the distance between assume-guarantee contracts. Additionally, it has been utilized to detect bugs in some of the most commonly used SAT solvers [3] within the SE and formal methods communities