University of Leicester
Browse
- No file added yet -

Faster temporal reasoning for infinite-state programs

Download (342.2 kB)
report
posted on 2014-02-20, 14:08 authored by Nir Piterman, Byron Cook, Heidy Khlaaf
In many model checking tools that support temporal logic, performance is hindered by redundant reasoning performed in the presence of nested temporal operators. In particular, tools supporting the state-based temporal logic CTL often symbolically partition the system's state space using the sub-formulae of the input temporal formula. This can lead to repeated work when tools are applied to infinite-state programs, as often the characterization of the state-spaces for nearby program locations are similar and interrelated. In this paper, we describe a new symbolic procedure for CTL verification of infinite-state programs. Our procedure uses the structure of the program's control-flow graph in combination with the nesting of temporal operators in order to optimize reasoning performed during symbolic model checking. An experimental evaluation against competing tools demonstrates that our approach not only gains orders-of-magnitude performance speed improvement, but allows for scalability of temporal reasoning for larger programs.

History

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Science

Source

University of Leicester

Copyright date

2014

Available date

2014-02-20

Publisher version

https://www2.le.ac.uk/departments/computer-science/documents/publications/2014

Book series

Computer science report;CS-14-01

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    No categories selected

    Keywords

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC