T. Chen, B. Ploeger, J. van de Pol & T. A. C. Willemse (2007):
Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems.
In: Proceedings of the 18th International Conference on Concurrency Theory (CONCUR'07),
LNCS 4703.
Springer,
Berlin, Heidelberg,
pp. 120–135,
doi:10.1007/978-3-540-74407-8_9.
E. Clarke, O. Grumberg, S. Jha, Y. Lu & H. Veith (2003):
Counterexample-guided Abstraction Refinement for Symbolic Model Checking.
Journal of ACM 50(5),
pp. 752–794,
doi:10.1145/876638.876643.
E. M. Clarke, Jr., O. Grumberg & D. A. Peled (1999):
Model Checking.
MIT Press,
Cambridge, MA, USA.
S. Cranen, B. Luttik & T. A. C. Willemse (2013):
Proof Graphs for Parameterised Boolean Equation Systems.
In: Proc. of the 24th International Conference on Concurrency Theory, (CONCUR 2013),
LNCS 8052.
Springer,
pp. 470–484,
doi:10.1007/978-3-642-40184-8_33.
L. De Moura & N. Bjørner (2008):
Z3: An Efficient SMT Solver.
In: Proc. of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08),
LNCS 4963.
Springer,
Berlin, Heidelberg,
pp. 337–340,
doi:10.1007/978-3-540-78800-3_24.
E. A. Emerson & C. S. Jutla (1991):
Tree automata, mu-calculus and determinacy.
In: Foundations of Computer Science, 1991. Proceedings, 32nd Annual Symposium on.
IEEE,
pp. 368–377,
doi:10.1109/SFCS.1991.185392.
E. Grädel, P. G. Kolaitis, L. Libkin, M. Marx, J. Spencer, M. Y. Vardi, Y. Venema & S. Weinstein (2007):
Finite Model Theory and Its Applications.
Texts in Theoretical Computer Science. An EATCS Series.
Springer,
doi:10.1007/3-540-68804-8.
S. Graf & H. Saidi (1997):
Construction of Abstract State Graphs with PVS.
In: Proc. of the 9th International Conference Computer Aided Verification (CAV'97),
LNCS 1254.
Springer,
pp. 72–83,
doi:10.1007/3-540-63166-6_10.
J. F. Groote & T. Willemse (2004):
Parameterised Boolean Equation Systems.
In: Proc. of 15th International Conference on Concurrency Theory (CONCUR 2004),
LNCS 3170.
Springer,
pp. 308–324,
doi:10.1007/978-3-540-28644-8_20.
J. F. Groote & T. A. C. Willemse (2005):
Model-checking Processes with Data.
Science of Computer Programming 56(3),
pp. 251–273,
doi:10.1016/j.scico.2004.08.002.
J. F. Groote & T. A. C. Willemse (2005):
Parameterised Boolean Equation Systems.
Theoretical Computer Science 343(3),
pp. 332–369,
doi:10.1016/j.tcs.2005.06.016.
J. F. Groote & T. A. C. Willemse (2004):
A Checker for Modal Formulae for Processes with Data.
In: Proc. of the 2nd International Symposium on Formal Methods for Components and Objects (FMCO 2003),
LNCS 3188.
Springer,
pp. 223–239,
doi:10.1007/978-3-540-30101-1_10.
R. P. J. Koolen, T. A. C. Willemse & H. Zantema (2015):
Using SMT for Solving Fragments of Parameterised Boolean Equation Systems.
In: Proc. of the 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015),
LNCS 9364.
Springer,
pp. 14–30,
doi:10.1007/978-3-319-24953-7_3.
Y. Nagae, M. Sakai & H. Seki (2017):
An Extension of Proof Graphs for Disjunctive Parameterised Boolean Equation Systems.
Electronic Proceedings in Theoretical Computer Science 235,
pp. 46–61,
doi:10.4204/EPTCS.235.4.
S. Orzan, W. Wesselink & T. A. C. Willemse (2009):
Static Analysis Techniques for Parameterised Boolean Equation Systems.
In: Proc. of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009),
LNCS 5505.
Springer,
pp. 230–245,
doi:10.1007/978-3-642-00768-2_22.
B. Ploeger, J. W. Wesselink & T. A. C. Willemse (2011):
Verification of Reactive Systems via Instantiation of Parameterised Boolean Equation Systems.
Information and Computation 209(4),
pp. 637–663,
doi:10.1016/j.ic.2010.11.025.
M. Presburger (1929):
Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen.
In: welchem die Addition als einzige Operation hervortritt, C. R. ler congrès des Mathématiciens des pays slaves, Warszawa,
pp. 92–101.
eptcs@eptcs.org