×

Model checking LTL with regular valuations for pushdown systems. (English) Zbl 1078.68081

Summary: Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures, and the model-checking problem for LTL has received special attention. However, all these works impose a strong restriction on the possible valuations of atomic propositions: whether a configuration of the pushdown system satisfies an atomic proposition or not can only depend on the current control state of the pushdown automaton and on its topmost stack symbol. We consider LTL with regular valuations: the set of configurations satisfying an atomic proposition can be an arbitrary regular language. The model-checking problem is solved via two different techniques, with an eye on efficiency. The resulting algorithms are polynomial in certain measures of the problem which are usually small, but can be exponential in the size of the problem instance. However, we show that this exponential blowup is inevitable. The extension to regular valuations allows to model problems in different areas; for instance, we show an application to the analysis of systems with checkpoints. We claim that our model-checking algorithms provide a general, unifying and efficient framework for solving them.

MSC:

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

Software:

Bebop
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Ball, T.; Rajamani, S.K., Bebop: a symbolic model checker for Boolean programs, (), 113-130 · Zbl 0976.68540
[2] Besson, F.; Jensen, T.; Métayer, D.L.; Thorn, T., Model checking security properties of control flow graphs, J. comput. secur., 9, 217-250, (2001)
[3] Bouajjani, A.; Esparza, J.; Maler, O., Reachability analysis of pushdown automata: application to model checking, (), 135-150
[4] Burkart, O.; Steffen, B., Model checking the full modal mu-calculus for infinite sequential processes, (), 419-429 · Zbl 1401.68188
[5] E.A. Emerson, Temporal and modal logic, Handbook Theor. Comp. Sci. B, 1991
[6] Emerson, E.A.; Lei, C., Modalities for model checking: branching time logic strikes back, Sci. comput. program., 8, 3, 275-306, (1987) · Zbl 0615.68019
[7] Esparza, J.; Hansel, D.; Rossmanith, P.; Schwoon, S., Efficient algorithms for model checking pushdown systems, (), 232-247 · Zbl 0974.68116
[8] Esparza, J.; Knoop, J., An automata-theoretic approach to interprocedural data-flow analysis, (), 14-30
[9] J. Esparza, A. Kučera, S. Schwoon, Model-checking LTL with regular valuations for pushdown systems, Technical Report EDI-INF-RR0044, Division of Informatics, University of Edinburgh, 2001 · Zbl 1087.68542
[10] Esparza, J.; Schwoon, S., A BDD-based model checker for recursive programs, (), 324-336 · Zbl 0991.68539
[11] Finkel, A.; Willems, B.; Wolper, P., A direct symbolic approach to model checking pushdown systems, Electronic notes theor. comput. sci., 9, (1997) · Zbl 0907.68126
[12] Jensen, T.; Le Métayer, D.; Thorn, T., Verification of control flow based security properties, (), 89-103
[13] Vardi, M.Y.; Wolper, P., Automata theoretic techniques for modal logics of programs, J. comput. syst. sci., 32, 183-221, (1986) · Zbl 0622.03017
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.