Show simple item record

dc.contributor.advisor Vardi, Moshe Y.
dc.creatorRozier, Kristin Yvonne
dc.date.accessioned 2013-07-24T19:46:44Z
dc.date.accessioned 2013-07-24T19:46:47Z
dc.date.available 2013-07-24T19:46:44Z
dc.date.available 2013-07-24T19:46:47Z
dc.date.created 2012-12
dc.date.issued 2013-07-24
dc.date.submitted December 2012
dc.identifier.urihttps://hdl.handle.net/1911/71687
dc.description.abstract Formal verification techniques are growing increasingly vital for the development of safety-critical software and hardware in practice. Techniques such as requirements-based design and model checking for system verification have been successfully used to verify systems for air traffic control, airplane separation assurance, autopilots, CPU logic designs, life-support, medical equipment, and other functions that ensure human safety. Formal behavioral specifications written early in the system-design process and communicated across all design phases increase the efficiency, consistency, and quality of the system under development. We argue that to prevent introducing design or verification errors, it is crucial to test specifications for satisfiability. We advocate for the adaptation of a new sanity check via satisfiability checking for property assurance. Our focus here is on specifications expressed in Linear Temporal Logic (LTL). We demonstrate that LTL satisfiability checking reduces to model checking and satisfiability checking for the specification, its complement, and a conjunction of all properties should be performed as a first step to LTL model checking. We report on an experimental investigation of LTL satisfiability checking. We introduce a large set of rigorous benchmarks to enable objective evaluation of LTL-to-automaton algorithms in terms of scalability, performance, correctness, and size of the automata produced. For explicit model checking, we use the Spin model checker; we tested all LTL-to-explicit automaton translation tools that were publicly available when we conducted our study. For symbolic model checking, we use CadenceSMV, NuSMV, and SAL-SMC for both LTL-to-symbolic automaton translation and to perform the satisfiability check. Our experiments result in two major findings. First, scalability, correctness, and other debilitating performance issues afflict most LTL translation tools. Second, for LTL satisfiability checking, the symbolic approach is clearly superior to the explicit approach. Ironically, the explicit approach to LTL-to-automata had been heavily studied while only one algorithm existed for LTL-to-symbolic automata. Since 1994, there had been essentially no new progress in encoding symbolic automata for BDD-based analysis. Therefore, we introduce a set of 30 symbolic automata encodings. The set consists of novel combinations of existing constructs, such as different LTL formula normal forms, with a novel transition-labeled symbolic automaton form, a new way to encode transitions, and new BDD variable orders based on algorithms for tree decomposition of graphs. An extensive set of experiments demonstrates that these encodings translate to significant, sometimes exponential, improvement over the current standard encoding for symbolic LTL satisfiability checking. Building upon these ideas, we return to the explicit automata domain and focus on the most common type of specifications used in industrial practice: safety properties. We show that we can exploit the inherent determinism of safety properties to create a set of 26 explicit automata encodings comprised of novel aspects including: state numbers versus state labels versus a state look-up table, finite versus infinite acceptance conditions, forward-looking versus backward-looking transition encodings, assignment-based versus BDD-based alphabet representation, state and transition minimization, edge abbreviation, trap-state elimination, and determinization either on-the-fly or up-front using the subset construction. We conduct an extensive experimental evaluation and identify an encoding that offers the best performance in explicit LTL model checking time and is constantly faster than the previous best explicit automaton encoding algorithm.
dc.format.mimetype application/pdf
dc.language.iso eng
dc.subjectLinear temporal logic
LTL
Model checking
Explicit model checking
Symbolic model checking
Ltl satisfiability checking
Specification debugging
Property assurance
PANDA
Symbolic Automata
LTL-to-automata
dc.title Explicit or Symbolic Translation of Linear Temporal Logic to Automata
dc.contributor.committeeMember Kavraki, Lydia E.
dc.contributor.committeeMember Varman, Peter J.
dc.date.updated 2013-07-24T19:46:47Z
dc.identifier.slug 123456789/ETD-2012-12-227
dc.type.genre Thesis
dc.type.material Text
thesis.degree.department Computer Science
thesis.degree.discipline Engineering
thesis.degree.grantor Rice University
thesis.degree.level Doctoral
thesis.degree.name Doctor of Philosophy
dc.identifier.citation Rozier, Kristin Yvonne. "Explicit or Symbolic Translation of Linear Temporal Logic to Automata." (2013) Diss., Rice University. https://hdl.handle.net/1911/71687.


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record