Model-Checking LTL with Regular Valuations for Pushdown Syst

Division of Informatics,University of Edinburgh

Division of Informatics August2001 398d881052d380eb62946def/

Model-Checking LTL with Regular Valuations for

Pushdown Systems

Stefan Schwoon,Javier Esparza,Antonin Kucera

Informatics Research Report EDI-INF-RR-0044

DIVISION of INFORMATICS

Laboratory for Foundations of Computer Science

August2001

To appear in Proceedings of TACS2001.

Abstract:

Recent works have proposed pushdown systems as a tool for analyzing programs with(recursive)procedures.In particular,the model-checking problem for LTL has been studied.In this paper we examine an extension of this, namely model-checking with regular valuations.The problem is solved via two different techniques,with an eye on ef?ciency–both techniques can be shown to be essentially optimal.Our methods are applicable to problems in different areas,e.g.,data-?ow analysis,analysis of systems with checkpoints,etc.,and provide a general,unifying and ef?cient framework for solving these problems.

Keywords:Model-checking,pushdown systems,LTL,CTL*,data-?ow analysis

Copyright c2001by The University of Edinburgh.All Rights Reserved

The authors and the University of Edinburgh retain the right to reproduce and publish this paper for non-commercial purposes.

Permission is granted for this report to be reproduced by others for non-commercial purposes as long as this copy-right notice is reprinted in full in any reproduction.Applications to make other use of the material should be addressed in the?rst instance to Copyright Permissions,Division of Informatics,The University of Edinburgh,80South Bridge, Edinburgh EH11HN,Scotland.

Model-Checking LTL with Regular Valuations for Pushdown Systems

Javier Esparza Division of Informatics University of Edinburgh Edinburgh EH93JZ

United Kingdom

Anton′?n Ku3c era

Faculty of Informatics MU

Botanick′a68a

60200Brno

Czech Republic

Stefan Schwoon

Institute for Informatics TUM

Arcisstr.21

80290Munich

Germany

August20,2001

Abstract

Recent works have proposed pushdown systems as a tool for analyzing programs with(recursive)procedures.In particular,the model-checking problem for LTL has been studied.In this paper we examine an extension of this,

namely model-checking with regular valuations.The problem is solved via two different techniques,with an eye

on ef￡ciency–both techniques can be shown to be essentially optimal.Our methods are applicable to problems in

different areas,e.g.,data-¤ow analysis,analysis of systems with checkpoints,etc.,and provide a general,unifying

and ef￡cient framework for solving these problems.

1Introduction

Pushdown systems can be seen as a natural abstraction of programs written in procedural,sequential languages such as C.They generate in￡nite-state transition systems whose states are pairs consisting of a control location(which stores global information about the program)and stack content(which keeps the track of activation records,i.e.,previously called procedures and their local variables).

Previous research has established applications of pushdown systems for the analysis of Boolean Programs[1,8] and certain data-¤ow analysis problems[7].The model-checking problem has been considered for various logics,and quite ef￡cient algorithms have emerged for linear time logics[2,6,9].

In this paper we revisit the model-checking problem for LTL and pushdown systems.Generally speaking,the problem is undecidable for arbitrary valuations,i.e.,the functions that map the atomic propositions of a formula to the respective sets of pushdown con￡gurations that satisfy them.However,it remains decidable for some restricted classes of valuations.In[2,6,9]valuations were completely determined by the control location and/or the topmost stack symbol(we call these valuations‘simple’in the following).Here we propose(and solve)the problem for valuations depending on regular predicates over the complete stack content.We argue that this solution provides a general,ef￡cient,and unifying framework for problems from different areas(e.g.,data-¤ow analysis,analysis of systems with checkpoints,etc.)

We proceed as follows:Section2contains basic de￡nitions.Most technical content is in Section3where we formally de￡ne simple and regular valuations and propose our solutions to the model-checking problem with regular This work was partially supported by the project“Advanced Validation Techniques for Telecommunication Protocols”of the Information Societies Technology Programme of the European Union.

On leave at the Institute for Informatics,TU Munich.Supported by a Research Fellowship granted by the Alexander von Humboldt Foundation and by a grant GA3CR No.201/00/1023.

On leave at LFCS,Division of Informatics,University of Edinburgh.

1

valuations,based on a reduction to the case of simple valuations.We can thus re-use most of the theory from[6].

While the reduction itself is based on a standard method,we pay special attention to ensure its ef￡ciency,modifying

the algorithm of[6]to take advantage of speci￡c properties of our constructions.We propose two different techniques

–one for regular valuations in general and another for a restricted subclass–both of which increase the complexity by

only a linear factor(in the size of an automaton for the atomic regular predicates).By contrast,a blunt reduction and

analysis would yield up to a quadric(‘’)blowup.Even though one technique is more powerful than the other at the same asymptotic complexity,we present them both since it is not clear how they might perform in practice.

In Section4we consider applicability of our abstract results.The￡rst area(Section4.1)are problems of interpro- …… 此处隐藏：54672字，全部文档内容请下载后查看。喜欢就下载吧 ……