How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors
Citations Over TimeTop 10% of 2006 papers
Abstract
Distributed automata-based LTL model-checking relies on algorithms for finding accepting cycles in a Büchi automaton. The approach to distributed accepting cycle detection as presented in [L. Brim, I. Černá, P. Moravec, J. Šimša. Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. In Formal Methods in Computer-Aided Design (FMCAD'04), volume 3312 of LNCS, pages 352–366. Springer, 2004] is based on maximal accepting predecessors. The ordering of accepting states (hence the maximality) is one of the main factors affecting the overall complexity of model-checking as an imperfect ordering can enforce numerous re-explorations of the automaton. This paper addresses the problem of finding an optimal ordering, proves its hardness, and gives several heuristics for finding an optimal ordering in the distributed environment. We compare the heuristics both theoretically and experimentally to find out which of these work well.
Related Papers
- → Robust Model-Checking of Linear-Time Properties in Timed Automata(2006)29 cited
- → Real-time symbolic model checking for hard real-time systems(2003)4 cited
- Robust model-checking of linear-time properties in timed automata(2006)
- → Automatic Verification, Performance Analysis, Synthesis and Optimization of Timed Systems(2016)1 cited
- A Theoretical Research on Water Resource Imperfect(2001)