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-

cedural data-¤ow analysis.Here,regular valuations can be used to‘gather’pieces of information which dynamically

depend on the history of procedure calls.LTL can express quite complex relationships among those dynamic properties

and allows to solve relatively complicated problems using our model-checking algorithm.To give a concrete example,

we indicate how to decide whether a given variable is dead at a given point of a recursive program with dynamic scoping.Another application(Section4.2)is connected to systems with checkpoints.First,we introduce a formal model for such systems,called pushdown systems with checkpoints.The idea is that the computation is interrupted at certain points and some property of the stack content is checked.Further computational steps depend on the result of this inspection.This part of our work is motivated by the advent of programming languages which can enforce security requirements.Newer versions of Java,for instance,enable programs to perform local security checks in which the methods on the stack are checked for correct permissions.Jensen et al[10]￡rst proposed a formal framework for such systems.With their techniques one can prove the validity of control¤ow based global security properties as well as to detect(and remove)redundant checkpoints.Our methods are more general,however;for instance,we are not restricted to safety properties,and our model can represent data-¤ow as well.Properties of pushdown systems with checkpoints can be expressed in LTL for which we provide an ef￡cient model-checking algorithm.In Section4.3we present and analyze a model-checking algorithm for CTL.In the context of￡nite-state systems it is well-known that model-checking the more powerful logic CTL can be reduced to checking LTL[5].This technique can be transferred to pushdown systems using model-checking with regular valuations.

The complexity of all of the previously developed algorithms is measured in certain parameters of the problem

which are usually small,and our complexity bounds are polynomials in those parameters.In general,those parameters

can be exponential in the size of a problem instance.Therefore,it is natural to ask whether it is possible to solve some

of the studied problems more ef￡ciently by other(possibly quite different)techniques.This question is answered

(negatively)in Section5where we establish EXPTIME lower bounds for those problems(even for rather restricted

forms of them).Hence,all of our algorithms are essentially 398d881052d380eb62946defplexity measures are discussed in more

detail in Remark3.1and in Section5.We draw our conclusions in Section6.

2Preliminaries

2.1Transition Systems

A transition system is a triple where is a set of states,is a transition relation,and

is a distinguished state called root.

As usual,we write instead of.The re¤exive and transitive closure of is denoted by.We say that a state is reachable from a state if.A state is reachable if it is reachable from the root.

A run of is an in￡nite sequence of states such that for each.Observe that an arbitrary suf￡x of a run is again a run–for every we de￡ne the suf￡x of,denoted,to be the run

2.2The Logic LTL

Let be a(countable)set of atomic propositions.LTL formulae are built according to the following abstract syntax equation(where ranges over):

Let be a transition system.A valuation of atomic propositions is a function.The validity of an LTL formula for a run w.r.t.a valuation,denoted,is de￡ned inductively on the structure of as follows:

2

and

We also de￡ne and.An LTL formula is valid in a state w.r.t.,written,iff for each run which starts in the state.

2.3Pushdown systems

A pushdown system is a tuple where is a￡nite set of control locations,is a￡nite stack alphabet,is a￡nite set of transition rules,is an initial control location,and

is a bottom stack symbol.

We use Greek letters to denote elements of,and small letters from the end of the alphabet to denote elements of.We also adopt a more intuitive notation for transition rules,writing instead of .

A con￡guration of is an element of.To we associate a unique transition system whose states are con￡gurations of,the root is,and the transition relation is the least relation satisfying the following:

for every

Without loss of generality we require that is never removed from the stack,i.e.,whenever then is of the form.

Pushdown systems can be conveniently used as a model of recursive sequential programs.In this setting,the (abstracted)stack of activation records increases if a new procedure is invoked,and decreases if the current procedure terminates.In particular,it means that the height of the stack can increase at most by one in a single transition. Therefore,from now on we assume that all pushdown systems we work with have this property.This assumption does not in¤uence the expressive power of pushdown systems,but it has some impact on the complexity analysis carried out in Section3.1.

3LTL on pushdown systems

Let be a pushdown system,an LTL formula,and a valuation.We deal with the following variants of the model checking problem:

(I)The model checking problem for the initial con￡guration:does?

(II)The global model checking problem:compute(a￡nite description of)the set of all con￡gurations,reachable or not,that violate.

(III)The global model checking problem for reachable con￡gurations:compute(a￡nite description of)the set of all reachable con￡gurations that violate.

In this paper we use so-called-automata to encode in￡nite sets of con￡gurations of a pushdown system.As we shall see,in some cases we can solve the problems(II)and(III)by computing-automata recognizing the above de￡ned sets of con￡gurations.

De￡nition3.1Let be a pushdown system.A-automaton is a tuple where is a￡nite set of states,(i.e.,the stack alphabet of)is the input alphabet,is the transition function,(i.e.,the set of control locations of)is the set of initial states,and is a￡nite set of accepting states.We extend to elements of in the standard way.A con￡guration of is recognized by iff .

3

In general,all of the above mentioned variants of the model checking problem are undecidable–if there are no ‘effectivity assumptions’about valuations(i.e.,if a valuation is an arbitrary function),one can easily express undecidable properties of pushdown con￡gurations just by atomic propositions.Therefore,we search for ‘reasonable’restrictions which do not limit the expressive power too much but allow to construct ef￡cient model-checking algorithms at the same time.For example,we can restrict ourselves to those valuations which are completely determined by associating atomic propositions with subsets of(see,e.g.,[2,6]).

De￡nition3.2Let be a pushdown system,a function.A simple valuation (speci￡ed by)is de￡ned as follows:.

In other words,(in)validity of an atomic proposition in a given con￡guration depends only on its control location and the topmost stack symbol(in our framework,we are mainly interested in reachable con￡gurations where the stack is always nonempty).Consequently,if we are given a pushdown system,an LTL formula,and a simple valuation ,we can easily synchronize with a B¨u chi automaton which recognizes exactly the models of,reducing the model-checking problem to the problem whether a given B¨u chi pushdown system has an accepting run[2,6].Here,it is crucial that atomic propositions are evaluated in a completely‘static’way because otherwise we could not perform the aforementioned synchronization.

In our paper,we propose a more general kind of valuations which are encoded by￡nite-state automata.We advocate this approach in the next sections by providing several examples of its applicability to practical problems; moreover,we show that this technique often results in rather ef￡cient(or,at least,essentially optimal)algorithms by presenting relevant complexity results.

De￡nition3.3Let be a pushdown system,a function which assigns to each pair of

a deterministic￡nite-state automaton over the alphabet with a total transition function;we also assume that the initial state of is not accepting.A regular valuation(speci￡ed by)is de￡ned as follows:where denotes the reverse of.

Hence,an atomic proposition is valid in a con￡guration iff the automaton enters a￡nal state after reading the stack contents bottom-up.As we shall see,the requirement that is deterministic is rather natural and has an important impact on complexity analysis.The assumption that the initial state of is not accepting simpli￡es our next constructions–as we already mentioned,we are only interested in reachable con￡gurations where it is impossible to empty the stack.Hence,this assumption does not bring any‘real’restrictions from a practical point of view.

3.1Model-Checking with Regular Valuations

The variants of the model checking problem de￡ned in the previous section have been considered in[6]for simple valuations.The following theorems are taken from there:

Theorem3.1Let be a pushdown system,an LTL formula,and a simple valuation.Let be a B¨u chi automaton for.Then one can compute

a-automaton with states and transitions in

time and space such that recognizes exactly the reachable con￡gurations of;

a-automaton of size in time using space such that recognizes exactly those con￡gurations of(reachable or not)such that;

a-automaton of size in time using

space such that recognizes exactly those reachable con￡gurations of such that.

Theorem3.2Let be a pushdown system,an LTL formula,and a simple valuation.Let be a B¨u chi automaton which corresponds to.

Problems(I)and(II)can be solved in time and space.

4

Problem(III)can be solved in either time and

space,or time and space.

Our aim here is to design ef￡cient model checking algorithms for regular valuations.We show that one can actually build on top of Theorem3.1.

For the rest of this section we￡x a pushdown system,an LTL formula,and a regular valuation.The B¨u chi automaton which corresponds to is denoted by.Let

be the subset of atomic propositions which appear in,and let be the deterministic￡nite-state automaton associated to for all and.Observe that we do not require the automata to be pairwise different;as we shall see in Section4.2,there are several‘safety’problems which can be reduced to the model-checking problem for pushdown systems and the LTL logic with regular valuations.In this case,many of the automata are identical and this fact substantially in¤uences the complexity.For simplicity,we assume that whenever or,then the and automata are either identical or have disjoint sets of states.Let be the set of all automata where and,and let be the set of states of

for each.The Cartesian product is denoted by.For given,,and ,we denote by the element of which appears in(observe that we can have even if or ).The vector of initial states(i.e.,the only element of where each component is an initial state of some )is denoted by.Furthermore,we write if for all,.Now we present and evaluate two techniques for solving the model checking problems with,,and.

Remark3.1(On the complexity measures)The size of an instance of the model-checking problem for pushdown systems and LTL with regular valuations is given by,where is the total size of all employed automata.However,in practice we usually work with small formulae and a small number of rather simple automata (see Section4);therefore,we measure the complexity of our algorithms in and rather than in and (in general,and can be exponentially larger than and).This allows for a detailed complexity analysis whose results better match the reality because and stay usually‘small’.This issue is discussed in greater detail in Section5where we provide some lower bounds showing that all algorithms developed in this paper are also essentially optimal from the point of view of worst-case analysis.

Technique1–extending the￡nite control

The idea behind this technique is to evaluate the atomic propositions‘on the¤y’by storing the(product of)automata in the￡nite control of and updating the vector of states after each transition according to the (local)change of stack contents.Note that here we conveniently use the assumptions that the automata are deterministic,have total transition functions,and read the stack bottom-up.However,we also need one additional assumption to make this construction work:

Each automaton is also backward deterministic,i.e.,for every and there is at most

one state such that.

Note that this assumption is truly restrictive–there are quite simple regular languages which cannot be recognized by ￡nite-state automata which are both deterministic and backward deterministic(as an example we can take the language ).

We de￡ne a pushdown system where,,and the transition rules are determined as follows:iff the following conditions hold:

,

there is such that and.

Observe that due to the backward determinism of there is at most one with the above stated properties;and thanks to determinism of we further obtain that for given and there is at most one such that.From this it follows that.

A con￡guration of is consistent iff(remember that is the vector of initial states of automata).In other words,is consistent iff‘re¤ects’the stack contents.Let be a con￡guration of and be the(unique)associated consistent con￡guration of.Now we can readily con￡rm that

5

(A)if,then where is consistent;

(B)if,then is consistent and is a transition of.

As the initial con￡guration of is consistent,we see(due to(B))that each reachable con￡guration of is consistent (but not each consistent con￡guration is necessarily reachable).Furthermore,due to(A)and(B)we also have the following:

(C)let be a con￡guration of(not necessarily reachable)and let be its associated consistent

con￡guration of.Then the parts of and which are reachable from and,respectively, are isomorphic.

The underlying function of the simple valuation is de￡ned by

if

otherwise

for all,.Now it is easy to see(due to(C))that for all and we have

where(1) During the construction of we observed that and.Applying Theorem3.2na¨?vely,we obtain that using Technique1,the model-checking problems(I)and(II)can be solved in cubic time and quadratic space(w.r.t.),and that model-checking problem(III)takes even quadric time and space.However,closer analysis reveals that we can do much better.

Theorem3.3Technique1(extending the￡nite control)gives us the following bounds on the model checking problems with regular valuations:

1.Problems(I)and(II)can be solved in time and space.

2.Problem(III)can be solved in either time and

space,or time and

space.

In other words,all problems take only linear(!)time and space in.Proof:We say that a-automaton is well-formed iff its set of states is of the form where is a set such that.A transition of a well-formed-automaton is consistent(w.r.t.)iff.A-automaton is consistent iff it is well-formed and contains only consistent transitions.

For the proof we revisit the algorithms presented in[6].Algorithm1shows the computation of from[6], restated for the special case of consistent-automata.We￡rst show that computation of upholds the consistency of a-automaton.

Lemma3.1When receiving a consistent-automaton as input,Algorithm1will output a consistent-automaton. Proof:Recall that Algorithm1implements the saturation procedure of[2],i.e.,all additions to the automaton corre-spond to the following situation:

If in and in the current automaton,then add a transition

.

From the existence of the transition rule in we know that there exists such that and .Provided that the automaton is consistent,we know that.Exploiting the backward determinism we get,and hence the added transition is consistent.

The fact that the algorithm only has to deal with consistent transitions in¤uences the complexity analysis: Lemma3.2Given a consistent-automaton,we can compute

in time and space.

6

Algorithm1

Input:a pushdown system;

a consistent-automaton

Output:the set of transitions of

1

2for all do;

3while do

4pop from trans;

5if then

6;

7for all do

8;

9for all do

10;

11for all do

12;

13return rel

Proof:A complete proof for the general case,discussing data structures and other details is given in[6].Here we just point out the important differences for the special case of consistent automata.

Line10will be executed once for every combination of a rule and a(consistent) transition.Since is the single state for which holds,there are

such combinations.Thus,the size of is also.

For the loop starting at line11,and(and hence)are￡xed,so line12is executed

times.

Line8is executed once for every combination of rules in and transitions .Since the size of is and is unique,we have such combinations.

Lemma3.3The repeating heads of the product of and can be computed in time and space.

Proof:(analogous to[6])The algorithm￡rst computes the set.Since this set can be represented by a consistent automaton with many states and no transitions,this step is bounded by the aforementioned limitations on time and space.From the results a head reachability graph of size is constructed.To￡nd the repeating heads,we identify the strongly connected components of that graph which takes time linear in its size.

We can now conclude the proof of Theorem3.3.The steps required to solve the model-checking problems are as follows:

Compute the set of repeating heads of the product of and.According to Lemma3.3,this takes

time and space,and we have.

Construct an automaton accepting exactly the consistent subset of.Take

.For every repeating head,add to the unique transition with.For every triple such that add to the transition

.There are at most such triples.This automaton is consistent and has states and transitions.

Compute the automaton corresponding to .According to Lemma3.2,this takes time and

space.(Recall that the size of is also a factor in the size of the product transition rules.)

7

Due to Lemma3.1,is consistent and accepts only consistent con￡gurations.According to Proposition3.1 in[6]we have for every con￡guration in.According to(1),we then have

for every in.Hence,we can solve the problem(II)by modifying slightly;let be the automaton where

.Problem(I)is solved by checking whether.Since none of the steps required to compute takes more than time and

space,the￡rst part of our theorem is proven.

To prove the second part we simply need to synchronise with the automaton which recognizes all reach-able con￡398d881052d380eb62946defputing takes time and space according to Theorem3.1.

The synchronization is performed as follows:For all transitions of and of we add a transition to the product.A straightforward procedure however would give us a higher result than necessary.We can do better by employing the following trick from[6]:￡rst all transitions of are sorted into buckets labelled by.Then each transition of is multiplied with the transitions in the respective bucket.As has states,each bucket contains items.Hence,the product can be computed in time and space.Alternatively,we can sort the transitions of into buckets of size(exploiting the consistency of)and construct the product in time and space.If we add the time and space which is needed to construct and,we get the results stated in the second part of Theorem3.3.

Technique2–extending the stack

An alternative approach to model-checking with regular valuations is to store the vectors of in the stack of. This technique works without any additional limitations,i.e.,we do not need the assumption of backward determinism of automata.

We de￡ne a pushdown system where,where is the vector of initial states of automata,and the set of transition rules is determined as follows:

Intuitively,the reason why we do not need the assumption of backward determinism in our second approach is that the stack carries complete information about the computational history of the automata.

A con￡guration is called consistent iff and for all

.

The underlying function of the simple valuation is de￡ned by

It is easy to see that where

is consistent.

Theorem3.4Technique2(extending the stack)gives us the same bounds on the model checking problems with regular valuations as Technique1,i.e.:

1.Problems(I)and(II)can be solved in time and space.

2.Problem(III)can be solved in either time and

space,or time and

space.

8

Proof:Since(here we use the fact that each is deterministic),we can compute a-automaton of size in time and space such that recognizes all con￡gurations of which violate(see Theorem3.1);

then,to solve problem(I),we just look if accepts.

The problem with is that it can also accept inconsistent con￡gurations of.Fortunately,it is possible to perform a kind of‘synchronization’with the reversed automata.We de￡ne where ,,and is de￡ned as follows:

if is a transition of,then contains a transition where;

if,,is a transition of,then is also a transition of.

Notice that is the same size as since in every transition is uniquely determined by and.Now,for every con￡guration,one can easily prove(by induction on)that

where for all

iff

where

From this we immediately obtain that indeed accepts exactly those con￡gurations of which violate.Moreover, the size of and the time and space bounds to compute it are the same as for which proves the￡rst part of the theorem.

To solve problem(III),one can try out the same strategies as in Theorem3.3.Again,it turns out that the most ef￡-cient way is to synchronize with the-automaton which recognizes all reachable con￡gurations of.Employing the same trick as in Theorem3.3(i.e.,sorting transitions of into buckets according to their labels),we obtain that the size of is and it can be computed in

time using 398d881052d380eb62946defing the alternative method(sorting transitions of into buckets instead and exploiting determinism)we get an automaton of size

in in time and space.

4Applications

4.1Interprocedural Data-Flow Analysis

Pushdown systems provide a very natural formal model for programs with recursive procedures.Hence,it should not be surprising that ef￡cient analysis techniques for pushdown automata can be applied to some problems of interpro-cedural data-¤ow analysis(see,e.g.,[7,11]).Here we brie¤y discuss the convenience of regular valuations in this application area.We do not present any detailed results about the complexity of concrete problems,because this would necessarily lead to a quite complicated and lengthy development which is beyond the scope of our work(though the associated questions are very interesting on their own).Our aim is just to provide convincing arguments demonstrating the importance of the technical results achieved in Section3.

A standard way of abstracting recursive programs for purposes of interprocedural data-¤ow analysis it to represent each procedure by its associated¤ow graph.Intuitively,the¤ow graph of is a labelled binary graph whose nodes correspond to‘program points’,and an arc indicates that the control¤ow is shifted from the point to by performing the instruction.The entry and exit points of are modeled by distinguished nodes.To avoid undecidabilities,the command(and related instructions)are modeled by nondeterminism,i.e.,there can be several arcs from the same node.Moreover,there are special arcs with labels of the form which model procedure calls(where is a vector of terms which are passed as parameters).Flow graphs can be easily translated to pushdown systems;as transitions of pushdown systems are not labelled,we￡rst perform a‘technical’modi￡cation of the¤ow graph,replacing each arc where is a nondeterministic node(i.e.,a node with more than one successor)by two arcs where is a new node and is a‘dummy’instruction without any effect.This allows to associate the instruction of each arc directly to(some nodes are associated to the dummy instruction).Now suppose there is a recursive system of procedures,where is a distinguished

9

starting procedure which cannot be called recursively.Their associated¤ow graphs can be translated to a pushdown automaton in the following way:

for each node of each¤owgraph we introduce a fresh stack symbol;

for each arc of the form we add a rule,where is the(only)control location;

for each arc of the form we add the rule where is the stack symbol for the entry node of(the¤ow graph of).Observe that one can also push special symbols correspond-ing to arguments if needed;

for each procedure different from we add the rule,where corresponds to the exit node of.For the starting procedure we add the rule.

In other words,the top stack symbol corresponds to the current program point(and to the instruction which is to be executed),and the stack carries the information about the history of activation calls.Now,many of the well-known properties of data-¤ow analysis(e.g.,liveness,reachability,very business,availability)can be expressed in LTL and veri￡ed by a model-checking algorithm(in some cases the above presented construction of a pushdown automaton must be modi￡ed so that all necessary information is properly re¤ected–but the principle is still the same).For example,if we want to check that a given variable is dead at a given program point(i.e.,whenever the program point is executed,in each possible continuation we have that is either not used or it is rede￡ned before it is used), we can model-check the formula

in the con￡guration,where,,and are atomic propositions which are valid in exactly those con￡gurations where the topmost stack symbol corresponds to the program point,to an instruction which uses the variable,or to an instruction which de￡nes,respectively.Even in this simple example,we can see that regular valuations are indeed useful–if we have a language with dynamic scoping(e.g.,LISP),we cannot resolve to which the instruction at a program point refers to without examining the stack of activation records(the refers to a local variable of the topmost procedure in the stack of activation records which declares it).So,and would be interpreted by regular valuations in this case.

The example above is quite simple.The‘real’power of regular valuations would become apparent in a context of more complicated problems where we need to examine complex relationships among dynamically gathered pieces of information.This is one of the subjects of intended future work.

4.2Pushdown Systems with Checkpoints

Another area where the results of Section3.1￡nd a natural application is the analysis of recursive computations with local security checks.Modern programming languages contain methods for performing run-time inspections of the stack of activation records,and processes can thus take dynamic decisions based on the gathered informa-tion.An example is the class implemented in Java Development Kit1.2offering the method which checks whether all methods stored in the stack are granted a given permission.If not,the method rises an exception.

We propose a(rather general)formal model of such systems called pushdown system with checkpoints.Our work was inspired by the paper[10]which deals with the same problem.Our model is more general,however.The model of[10]is suitable only for checking safety properties,does not model data-¤ow,and forbids mutually recursive procedure calls whereas our model has none of these restrictions.Properties of pushdown systems with checkpoints can be expressed in LTL and we provide an ef￡cient model-checking algorithm for LTL with regular valuations.

De￡nition4.1A pushdown system with checkpoints is a triple where

is a pushdown system,

is a function with domain which assigns to each pair a deterministic￡nite-state automaton.For technical convenience,we assume that is total,,and

.Elements of are called checkpoints.

10

is a function which partitions the set of transition rules into positive,negative,and inde-pendent ones.We require that if is not a checkpoint,then all rules of the form are independent.

The function determines whether a rule can be applied when an inspection of the stack at a checkpoint yields a positive or negative result,or whether it is independent of such 398d881052d380eb62946defing positive and negative rules,we can model systems which perform commands where the condition is based on dynamic checks;hence,these checks can be nested to an arbitrary level.The fact that a rule is positive,negative,or independent is denoted by,,or,respectively.

To we associate a unique transition system where the set of states is the set of all con￡gurations of,

is the root,and the transition relation is the least relation satisfying the following:

if,then for all s.t.;

if,then for all s.t.;

if,then for all.

Some natural problems for pushdown processes with checkpoints are listed below.

The reachability problem:given a pushdown system with checkpoints,is a given con￡guration reachable?

The checkpoint-redundancy problem:given a pushdown system with checkpoints and a checkpoint,is there a reachable con￡guration where the checkpoint is(or is not)satis￡ed?

This problem is important because redundant checkpoints can be safely removed together with all negative(or positive)rules,declaring all remaining rules as independent.Thus,one can decrease the runtime overhead.

The global safety problem:given a pushdown system with checkpoints and a formula of LTL,do all reachable con￡gurations satisfy?

An ef￡cient solution to this problem allows to make‘experiments’with checkpoints with the aim of￡nding a solution with a minimal runtime overhead.

Actually,it is quite easy to see that all these problems(and many others)can be encoded by LTL formulae and regular valuations.For example,to solve the reachability problem,we take a predicate which is satis￡ed only by the con￡guration whose reachability is in question(the associated automaton has states)and then we check the formula.Observe that this formula in fact says that is unreachable;the reachability itself is not directly expressible in LTL(we can only say that is reachable in every run).However,it does not matter because we can simply negate the answer of the model-checking algorithm.

4.2.1Model-Checking LTL for Pushdown Systems with Checkpoints

Let be a pushdown system with checkpoints,where.We de￡ne a pushdown system where is the least set of rules satisfying the following(for each );

if,then;

if,then;

if,then.

Intuitively,behaves in the same way as the underlying pushdown system of,but it also‘remembers’what kind of rule(positive,negative,independent)was used to enter the current con￡guration.

Let be a regular valuation for con￡gurations of with an underlying function(see De￡nition3.3),and let be an LTL formula.Let,,and be fresh atomic propositions which do not appear in.We de￡ne a function,which is the underlying function for a regular valuation for con￡gurations of,as follows: if,then for

11

for,where is the product automaton accepting where is a checkpoint

,where is a one-state automaton accepting.

,where is a one-state automa-ton accepting.

Now we can readily con￡rm the following:

Theorem4.1Let be a con￡guration of.We have that

where.

Proof:It suf￡ces to realize that

is an in￡nite path in iff

is an in￡nite path in satisfying(where each for is either,,or;realize that all are determined uniquely).Indeed,ensures that all transitions in the latter path are‘consistent’with possible checkpoints in the former path.As all atomic propositions which appear in are evaluated identically for pairs,

(see the de￡nition of above),we can conclude that both paths either satisfy or do not satisfy.

The previous theorem in fact says that the model-checking problem for LTL and pushdown systems with check-points can be reduced to the model-checking problem for LTL and‘ordinary’pushdown systems.As the formula is￡xed and the atomic propositions,,and are regular,we can evaluate the complexity bounds for the resulting model-checking algorithm using the results of Section3.1.Let be the set of all atomic propositions which appear in,and let be the set of all automata.Let be the Cartesian product of the sets of states of all automata and the automata of.Let be a B¨u chi automaton which corresponds to.Now we can state our theorem(remember that is the set of control states and the set of rules of the underlying pushdown system of).

Theorem4.2We have the following bounds on the model checking problems for LTL with regular valuations and pushdown systems with checkpoints:

1.Problems(I)and(II)can be solved in time and space.

2.Problem(III)can be solved in either time and

space,or time and

space.

Proof:We apply Theorem4.1,which says that we can equivalently consider the model-checking problem for the pushdown system,formula,and valuation.First,let us realize that the B¨u chi automaton which corresponds to can be actually obtained by‘synchronizing’with the B¨u chi automaton for,because .As the formula is￡xed,the synchronization increases the size of just by a constant factor. Hence,the automaton for is asymptotically of the same size of.The same can be said about the sizes of and,and about the sizes of and.Moreover,if we collect all automata in the range of(see above)and consider the state space of their product,we see that it has exactly the size of because the automata associated to and have only one state.

12

4.3Model-checking CTL

In this section,we apply the model-checking algorithm to the logic CTL which extends LTL with existential path quanti￡cation[4].More precisely,CTL formulae are built according to the following abstract syntax equation:

where ranges over the atomic propositions(interpreted,say,by a regular valuation represented by a￡nite automaton of size).

For￡nite-state systems,model-checking CTL can be reduced to checking LTL as follows[5]:For a CTL formula,call the path depth of the maximal nesting depth of existential path quanti￡ers within.Subformulae of can be checked in ascending order of path depth;subformulae of the form where is-free are checked with an LTL algorithm which returns the set of states satisfying.Then is replaced by a fresh atomic proposition whose valuation yields true exactly on,and the procedure is repeated for subformulae of higher path depth.The method can be transferred to the case of pushdown systems;running the LTL algorithm on returns an automaton.We can then replace by a fresh atomic proposition whose valuation is given by.This method was already proposed in[9],but without any complexity analysis.

Let us review the complexity of this procedure.For the rest of this subsection￡x a pushdown system .Given an-free formula,let be a B¨u chi automaton corresponding to,and let be the size of the automata encoding the regular valuations of propositions in.

The algorithms from section3.1(in general we can only use Technique2)yield an automaton which accepts exactly the con￡gurations satisfying.Observe that is non-deterministic,reads the stack top-down,and has states.We need to modify the automaton before we can use it as an encoding for the regular valuation of.More precisely,we need to reverse the automaton(i.e.make it read the stack bottom-up)and then determinise it.Reversal does not increase the size,and due to the determinism of(in bottom-up direction)the determinisation explodes only the‘part’of the states,i.e.we get an automaton of size.

To check subformulae of higher path depth we replace by a fresh atomic proposition.With we associate the automaton which is a copy of where the set of accepting states is taken as

.The cross product of these new automata with the‘old’automata takes only states again;we need just one copy of the new automaton,and all reachable states are of the form where and.

As we go up in path depth,we can repeat this procedure:First we produce a deterministic valuation automaton by taking the cross product of the automata corresponding the atomic propositions and those derived from model-checking formulae of lower path depth.Then we model-check the subformula currently under consideration,and reverse and determinise the resulting automaton.By the previous arguments,each determinisation only blows up the non-deterministic part of the automaton,i.e.after each stage the size of the valuation automaton increases by a factor of where is a B¨u chi automaton for the subformula currently under consideration.

With this in mind,we can compute the complexity for formulae of arbitrary path depth.Let be the B¨u chi automata corresponding to the inpidual subformulae of a formula.Adding the times for checking the subformulas and using Theorem3.4we get that the model-checking procedure takes at most

time and

space.The algorithm hence remains linear in both and.The algorithm of Burkart and Steffen[3],applied to CTL formulae which are in the second level of the alternation hierarchy,would yield an algorithm which is cubic in.On the other hand,the performance of our algorithm in terms of the formula is less clear.In practice,it would depend strongly on the size of the B¨u chi automata for the subformulae,and on the result of the determinisation procedures.

13

5Lower Bounds

In previous sections we established reasonably-looking upper bounds for the model-checking problem for pushdown systems(￡rst without and then also with checkpoints)and LTL with regular valuations.However,the algorithms are polynomial in,and not in the size of problem instance which is(as we already mentioned in Remark3.1).In Remark3.1we also explained why we use these parameters–it has been argued

that typical formulae(and their associated B¨u chi automata)are small,hence the size of is actually more relevant(a model-checking algorithm whose complexity is exponential just due to the blowup caused by the transformation of into is usually ef￡cient in practice).The same can be actually said about–in Section4we have seen that there are interesting practical problems where the size of does not explode.Nevertheless,from the point of view of worst-case analysis(where we measure the complexity in the size of problem instance)our algorithms are exponential.A natural question is whether this exponential blowup is indeed necessary,i.e.,whether we could(in principle)solve the model-checking problems more ef￡ciently by some‘better’technique.In this section we show it is not the case,because all of the considered problems are EXPTIME-hard(even in rather restricted forms).

We start with the natural problems for pushdown systems with checkpoints mentioned in the previous section(the reachability problem,the checkpoint redundancy problem,etc.)All of them can be(polynomially)reduced to the model-checking problem for pushdown systems with checkpoints and LTL with regular valuations and therefore are solvable in EXPTIME.The next theorem says that this strategy is essentially optimal,because even the reachability problem provably requires exponential time.

Theorem5.1The reachability problem for pushdown systems with checkpoints(even for those with just three control states and no negative rules)is EXPTIME-complete.

Proof:The membership to EXPTIME follows from Theorem4.2.We show EXPTIME-hardness by reduction from the acceptance problem for alternating LBA(which is known to be EXPTIME-complete).An alternating LBA is a tuple where and are de￡ned as for ordinary non-deterministic LBA(and are the left-end and right-end markers,resp.),and is a function which partitions the states of into universal,existential,accepting,and rejecting,respectively.We assume(w.l.o.g.)that is de￡ned so that ‘terminated’con￡gurations(i.e.,the ones from which there are no further computational steps)are exactly accepting and rejecting con￡gurations.Moreover,we also assume that always halts and that its branching degree is(i.e., each con￡guration has at most two immediate successors).A computational tree for on a word is any (￡nite)tree satisfying the following:the root of is(labeled by)the initial con￡guration of,and if is a node of labelled by a con￡guration where and,then the following holds:

if is accepting or rejecting,then is a leaf;

if is existential,then has one successor whose label is some con￡guration which can be reached from in one computational step(according to);

if is universal,then has successors where is the number of con￡gurations which can be reached from in one step;those con￡gurations are used as labels of the successors in one-to-one fashion.

accepts iff there is a computational tree such that all leaves of are accepting con￡gurations.

Now we describe a polynomial algorithm which for a given alternating LBA and a word of length constructs a pushdown system with checkpoints and its con￡guration such that is reachable from the initial con￡guration of iff accepts.Intuitively,the underlying system of simulates the execution of and checkpoints are used to verify that there is no cheating during the process.We start with the de￡nition of,putting where

contains the following(families of)rules:

1.

2.for all and

3.for every

14

4.for every

5.

6.,,,

7.for every

8.,,,

9.for every

10.,,,

Intuitively,the execution of starts by entering the state(rule1).Then,exactly symbols of are pushed to the stack;the compound symbol indicates that the tape contains the symbol and,if,that the head is at this position and the control state of is;if it means that the head is elsewhere.During this process,the family of symbols is used as a‘counter’(rules2).Realize that the word of length is surrounded by the‘’and‘’markers,so the total length of the con￡guration is.The last symbol is then rewritten to,where is one of(rules3).The purpose of is to keep information about the just stored con￡guration(whether it is existential,universal,accepting,or rejecting)and the index of a rule which is to be used to obtain the next con￡guration(always the￡rst one;remember that accepting and rejecting con￡gurations are terminal).After that,is successively rewritten to all of the symbols and disappears(rules4,5). Their only purpose is to invoke several consistency checks–as we shall see,each pair is a checkpoint and all rules of4,5are positive.Depending on the previously stored(i.e.,on the type of the just pushed con￡guration), we either continue with guessing the next one,or change the control state to or(if the con￡guration is accepting or rejecting,resp.)Hence,the guessing goes on until we end up with an accepting or rejecting con￡guration.This must happen eventually,because always halts.If we￡nd an accepting con￡guration,we successively remove all existential con￡gurations and those universal con￡guration for which we have already checked both successors.If we ￡nd a universal con￡guration with only one successor checked–it is recognized by the‘’symbol–we change ‘’to‘’and check the other successor(rules7and8).Similar things are done when a rejecting con￡guration is found.The control state is switched to and then we remove all con￡gurations until we(possibly)￡nd an existential con￡guration for which we can try out the other successor(rules9and10).We see that is accepted by iff we eventually pop the initial con￡guration when the control state is‘’,i.e.,iff the state is reachable.

To make all that work we must ensure that cannot gain anything by‘cheating’,i.e.,by pushing inconsistent sequences of symbols which do not model a computation of in the described way.This is achieved by declaring all pairs for as checkpoints.The automaton for accepts those words of the form,where,for every,such that the triples of symbols at positions in each pair of successive substrings are consistent with the symbol w.r.t.the transition function of(if some con￡guration has only one immediate successor,then ‘ignores’the rule index stored in).Furthermore,the￡rst con￡guration must be the initial one,and the last con￡guration must be consistent with.Observe that needs just states to store the two triples (after checking subwords,the triple of is‘forgotten’)the initial con￡guration,a‘counter’of capacity ,and some auxiliary information.Moreover,is deterministic and we can also assume that its transition function is total.As all rules associated with checkpoints are positive,any cheating move eventually results in entering a con￡guration where the system‘gets stuck’,i.e.,cheating cannot help to reach the con￡guration.

From the(technical)proof of Theorem5.1we can easily deduce the following:

Theorem5.2The model-checking problem(I)for pushdown systems with checkpoints(even for those with just three control states and no negative rules)is EXPTIME-complete even for a￡xed LTL formula￡n where￡n is an atomic predicate interpreted by a simple valuation.

Proof:Let us consider the pushdown system with checkpoints constructed in the proof of Theorem5.1. To ensure that each￡nite path in is a pre￡x of some run,we extend the set of transition rules of by a family of independent rules of the form for each control state and each stack symbol.Now it suf￡ces to realize that the initial con￡guration cannot reach the state iff it cannot reach any state of the form (where)iff￡n where is a simple valuation with the underlying function such that ￡n.

15

Hence,model-checking LTL for pushdown systems with checkpoints is EXPTIME-complete even when we have

only simple valuations.

Now we analyze the complexity of model-checking with(ordinary)pushdown systems and LTL formulae with

regular valuations.First,realize that if we take any￡xed formula and a subclass of pushdown systems where the

number of control states is bounded by some constant,the model-checking problem is decidable in polynomial time.

Now we prove that if the number of control states is not bounded,the model-checking problem becomes EXPTIME-

complete even for a￡xed formula.At this point,one is tempted to apply Theorem4.1to the formula￡n of

Theorem5.2.Indeed,it allows to reduce the model-checking problem for pushdown systems with checkpoints and ￡n to the model-checking problem for ordinary pushdown systems and another￡xed formula￡n. Unfortunately,this reduction is not polynomial because the atomic proposition occurring in is interpreted with the help of several product automata constructed out of the original automata which implement checkpoints(see

the previous section).Therefore we need one more technical proof.

Theorem5.3The model-checking problem(I)for pushdown systems and LTL formulae with regular valuations is

EXPTIME-complete even for a￡xed formula correct￡n.

Proof:This proof is similar to the proof of Theorem5.1.Again,we construct a pushdown system which simulates the execution of an alternating LBA on an input word of length.The difference is that,since there are no checkpoints,we must￡nd a new way of‘cheating-detection’,i.e.,we must be able to recognize situations when the next con￡guration of has not been guessed correctly.It is achieved by adding a family of control states;after guessing a new con￡guration,successively switches its control state to without modifying its stack.The underlying function of the constructed regular valuation assigns to each pair correct a deterministic automaton which checks that the triples of symbols at positions in each pair of successive con￡gurations previously pushed to the stack are‘consistent’(is almost the same automaton as the of the proof of Theorem5.1).All other pairs of the form correct are assigned an automaton accepting .The is formally de￡ned as follows:where

contains the following(families of)rules:

1.

2.for all and

3.for every

4.for every and

5.for every

6.,,,

7.for every

8.,,,

9.for every

10.,,,

11.for every control state and every.

Hence,the rules are almost the same as in the proof of Theorem5.1,except for some changes in3.,4.,5.,and11.The underlying function of the constructed regular valuation assigns to￡n an automaton recognizing all strings of where the last symbol is,and to all other pairs of the form￡n an automaton recognizing the empty language. We see that accepts iff there is an in￡nite path from the state such that correct holds in all states of the path and￡n holds in at least one state iff correct￡n where is the constructed regular valuation.

Observe that model-checking with pushdown systems and any￡xed LTL formula whose predicates are interpreted by a simple valuation is already polynomial(see Theorem3.1).

16

6Conclusion

We have presented two different techniques for checking LTL with regular valuations on pushdown systems.Both

techniques rely on a reduction to(and slight modi￡cation of)the problem for simple valuations discussed in[6].Both

techniques take linear time and space in where is the set of states of an automaton representing the regular predicates used in the formula.Since both take the same asymptotic time it would be interesting to compare

their ef￡ciency in practice(for cases where both techniques can be used).

The solution can be seamlessly combined with the concept of symbolic pushdown systems in[8].These are used

to achieve a succinct representation of Boolean Programs,i.e.,programs with(recursive)procedures in which all

variables are boolean.

The ability to represent data is a distinct advantage over the approaches hitherto made in our areas of application,

namely data-¤ow analysis[7]and security properties[10].For the latter,we have indicated that our model is more

general.Our approach provides a unifying framework for these applications without losing ef￡ciency.Both techniques

take linear time in whereas the methods used in[7]were cubic(though erroneously reported as linear there, too).In[10]no complexity analysis was conducted.

References

[1]T.Ball and S.K.Rajamani.Bebop:A symbolic model checker for boolean programs.In SPIN00:SPIN

Workshop,volume1885of LNCS,pages113–130.Springer,2000.

[2]A.Bouajjani,J.Esparza,and O.Maler.Reachability analysis of pushdown automata:Application to model

checking.In Proc.CONCUR’97,LNCS1243,pages135–150.

[3]O.Burkart and B.Steffen.Model checking the full modal mu-calculus for in￡nite sequential processes.In Proc.

ICALP’97,volume1256of LNCS,pages419–429.Springer,1997.

[4]E.A.Emerson.Temporal and modal logic.Handbook of Theoretical Comp.Sci.,B,1991.

[5]E.A.Emerson and C.Lei.Modalities for model checking:Branching time logic strikes back.Science of Com-

puter Programming,8(3):275–306,1987.

[6]J.Esparza,D.Hansel,P.Rossmanith,and S.Schwoon.Ef￡cient algorithms for model checking pushdown

systems.In Proc.CAV’00,LNCS1855,pages232–247.Springer,2000.

[7]J.Esparza and J.Knoop.An automata-theoretic approach to interprocedural data-¤ow analysis.In Proceedings

of FoSSaCS’99,volume1578of LNCS,pages14–30.Springer,1999.

[8]J.Esparza and S.Schwoon.A BDD-based model checker for recursive programs.In Proc.CAV’01,LNCS2102,

pages324–336.Springer,2001.

[9]A.Finkel,B.Willems,and P.Wolper.A direct symbolic approach to model checking pushdown systems.Elec-

tronic Notes in Theoretical Computer Science,9,1997.

[10]T.Jensen,D.Le M′e tayer,and T.Thorn.Veri￡cation of control¤ow based security properties.In IEEE Sympo-

sium on Security and Privacy,pages89–103,1999.

[11]B.Steffen,A.Cla?en,M.Klein,J.Knoop,and T.Margaria.The￡xpoint-analysis machine.In Proceedings of

CONCUR’95,volume962of LNCS,pages72–87.Springer,1995.

17

本文来源：https://www.bwwdw.com/article/nodl.html