Rabinizer: Small Deterministic Automata for LTL(F,G)

DOI10.1007/978-3-642-33386-6_7zbMath1374.68259OpenAlexW2293285880MaRDI QIDQ4649288

Jan Křetínský, Javier Esparza, Andreas Gaiser

Publication date: 21 November 2012

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-33386-6_7

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

From LTL to deterministic automata. A safraless compositional approach, Rabinizer, Back to the future: a fresh look at linear temporal logic

Uses Software

• PRISM
• BEEM
• LTL2BA
• ltl2dstar