Verification of non-regular program properties [Elektronische Ressource] / vorgelegt von Roland Axelsson

Roland Axelsson

Sujets

• Mathematics

Informations

• Publié par: ludwig-maximilians-universitat_munchen
• Publié le: 01 janvier 2010
• Nombre de lectures: 8
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Verification of Non-Regular Program
Properties
Roland Axelsson
Mu¨nchen 2010Verification of Non-Regular Program
Properties
Roland Axelsson
Dissertation
am Institut fu¨r Informatik
Ludwig–Maximilians–Universit¨at
Mu¨nchen
vorgelegt von
Roland Axelsson
Mu¨nchen, den 27.4.2010Erstgutachter: Prof. Dr. Martin Lange
Zweitgutachter: Prof. Dr. Thomas Wilke
Tag der mu¨ndlichen Pru¨fung: 25.6.2010Abstract
Most temporal logics which have been introduced and studied in the past decades can be
∗embedded into the modalL . This is the case for e.g. PDL, CTL, CTL , ECTL, LTL,
etc. and entails that these logics cannot express non-regular program properties. In recent
years, some novel approaches towards an increase in expressive power have been made:
Fixpoint Logic with Chop enrichesL with a sequential composition operator and thereby
allows to characterise context-free processes. The Modal Iteration Calculus uses inflation-
ary fixpoints to exceed the expressive power ofL . Higher-Order Fixpoint Logic (HFL)
incorporates a simply typedλ-calculus into a setting with extremal fixpoint operators and
even exceeds the expressive power of Fixpoint Logic with Chop. But also PDL has been
equipped with context-free programs instead of regular ones.
In terms of expressivity there is a natural demand for richer frameworks since program
property specifications are simply not limited to the regular sphere. Expressivity however
usually comes at the price of an increased computational complexity of logic-related deci-
sion problems. For instance are the satisfiability problems for the above mentioned logics
undecidable. Weinvestigate inthisworkthemodelchecking problemofthreedifferent log-
ics which are capable of expressing non-regular program properties and aim at identifying
fragments with feasible model checking complexity.
Firstly, we develop a generic method for determining the complexity of model checking
PDL over arbitrary classes of programs and show that the border to undecidability runs
between PDL over indexed languages and PDL over context-sensitive languages. It is
however still in PTIME for PDL over linear indexed languages and in EXPTIME for PDL
over indexed languages. We present concrete algorithms which allow implementations of
model checkers for these two fragments.
We then introduce an extension of CTL in which the until- and release- operators are
adorned with formal languages. These are interpreted over labeled paths and restrict
the moments on such a path at which the operators are satisfied. The until-operatoris for instance satisfied if some path prefix forms a word in the language it is adorned
with (besides the usual requirement that until that moment some property has to hold
and at that very moment some other property must hold). Again, we determine the
computational complexities of the model checking problems for varying classes of allowed
languages in either operator. It turns out that either enabling context-sensitive languages
in the until or context-free languages in the release- operator renders the model checking
problem undecidable while it is EXPTIME-complete for indexed languages in the until
and visibly pushdown languages in the release- operator. PTIME-completeness is a result
of allowing linear indexed languages in the until and deterministic context-free languages
in the release. We do also give concrete model checking algorithms for several interesting
fragments of these logics.
Finally, we turn our attention to the model checking problem of HFL which we have
already studied in previous works. On finite state models it is kEXPTIME-complete for
kHFL , the fragment of HFL obtained by restricting functions in theλ-calculus to order k.
Novel in this work is however the generalisation (from the first-order case to the case for
functions of arbitrary order) of an idea to improve the best and average case behaviour of
a model checking algorithm by using partial functions during the fixpoint iteration guided
by the neededness of arguments. This is possible, because the semantics of a closed HFL
formula is not a total function but the value of a function at some argument. Again, we
give a concrete algorithm for such an improved model checker and argue that despite the
very high model checking complexity this improvement is very useful in practice and gives
feasible results for HFL with lower order fuctions, backed up by a statistical analysis of
the number of needed arguments on a concrete example.
Furthermore,weshowhowHFLcanbeusedasatoolforthedevelopmentofalgorithms. Its
highexpressivity allowstoencodeawidevarietyofproblemsasinstancesofmodelchecking
already in the first-order fragment. The rather unintuitive – yet very succinct – problem
encoding together with an analysis of the behaviour of the above sketched optimisation
may give deep insights into the problem. We demonstrate this on the example of the
universality problem for nondeterministic finite automata, where a slight variation of the
optimised model checking algorithm yields one of the best known methods so far which
was only discovered recently.
We do also investigate typical model-theoretic properties for each of these logics and com-
pare them with respect to expressive power.Zuasmmenfassung
Die meisten Temporallogiken, welche in den vergangenen Jahrzehnten eingefu¨hrt und von
der Forschung beru¨cksichtigt wurden, lassen sich in den modalen-Kalku¨l einbetten. Dies
∗betrifft z.B. PDL, CTL, CTL , ECTL, LTL, etc. und beinhaltet, dass diese Logiken nicht
dazu in der Lage sind, nicht-regul¨are Programmeigenschaften auszudru¨cken.
In den letzten Jahren wurden allerdings eine Reihe ausdruckst¨arkerer Logiken entwickelt:
FixpointLogicwithChoperweitert den-Kalku¨lumeinen Operatorfu¨rsequentielle Kom-
position und erlaubt es dadurch, logische Charakterisierungen von kontextfreien Prozessen
anzugeben. Im Modal Iteration Calculus fu¨hren inflation¨are Fixpunkte dazu, dass seine
Ausdrucksst¨arke diejenige des -Kalku¨ls u¨bersteigt. Higher-Order Fixpoint Logic (HFL)
vereint in sich einen einfach getypten λ-Kalku¨l sowie kleinste und gr¨osste Fixpunktquan-
torenundistdamitsogarnochausdrucksst¨arker alsFixpointLogicwithChop. SelbstPDL
wurde in der Vergangenheit bereits mit kontextfreien anstelle von regul¨aren Programmen
untersucht.
Da Spezifikationen von Programmeigenschaften nicht auf Regularit¨at beschr¨ankt sind,
ergibtsicheinnatu¨rlicherBedarfanausdrucksst¨arkerenSpezifikationsformalismen. Gr¨ossere
Ausdrucksst¨arke ist jedoch u¨blicherweise mit einem Ansteigen der Komplexit¨at der im
Zusammenhang mit der Logik stehenden Entscheidungsprobleme verbunden. Beispiels-
weise sind die Erfu¨llbarkeitsprobleme fu¨rjede deroben genannten Logiken unentscheidbar.
Die vorliegende Arbeit untersucht die Model Checking Probleme von drei verschiedenen
Logiken, welche im Stande sind, nicht-regul¨are Eigenschaften auszudru¨cken und gibt Frag-
mente von ihnen an, welche eine in der Praxis noch verwertbare Komplexit¨at in Bezug auf
das Model Checking Problem besitzen.
Zun¨achst wird eine generische Methode entwickelt, um die Komplexit¨at des Model Check-
ing Problems von PDL u¨ber beliebigen Klassen von Programmen zu bestimmen. Es wird
gezeigt, dass die Grenze zur Unentscheidbarkeit zwischen PDL u¨ber indexierten Sprachen
und PDL u¨ber kontextsensitiven Sprachen verl¨auft. Fu¨r PDL u¨ber linear indexiertenviii
Sprachen ist das Problem noch immer in PTIME und fu¨r PDL u¨ber indexierten Sprachen
in EXPTIME. Wir geben fu¨r diese beiden Fragmente konkrete Algorithmen fu¨r eine Im-
plementierung an.
Im Anschluss fu¨hren wir eine Erweiterung von CTL ein, in welcher die until- und re-
lease-Operatoren mit formalen Sprachen ausgestattet sind. Diese Sprachen werden u¨ber
beschrifteten Pfaden interpretiert und kennzeichnen die Momente entlang solcher Pfade in
welchen dieOperatorenerfu¨lltseinmu¨ssen. Soistbeispielsweise deruntil-Operatorerfu¨llt,
falls es einen Pfadpr¨afix gibt, welcher ein Wort in der Sprache bildet, mit der der Oper-
ator ausgestattet ist (und die u¨bliche until-Bedingung gilt, n¨amlich, dass eine bestimmte
Eigenschaft injedem Zustand bis zu diesem Zeitpunkt gegoltenhat, sowie dass eine andere
in genau jenem Zeitpunkt gilt).
Wie im Fall von PDL, bestimmen wir die Komplexit¨at des Model Checking Problems fu¨r
verschiedene Klassen vonerlaubten Sprachen im jeweiligen Operator. Es stellt sich heraus,
dass sowohl die Klasse der kontextsensitiven Sprachen im until- als auch die Klasse der
kontextfreien Sprachen im release-Operator zu Unentscheidbarkeit des Model Checking
Problems fu¨hren. Es ist EXPTIME-vollst¨andig fu¨r indexierte Sprachen im until- und vis-
ibly pushdown Sprachen im release-Operator. Linear indexierte Sprachen im until sowie
deterministisch kontextfreie Sprachen im release fu¨hren zu einem PTIME-vollst¨andigen
Model Checking Problem. Wir geben ebenfalls wieder konkrete Model Checking Algorith-
men fu¨r ausgew¨ahlte Fragmente dieser Logiken an.
Schliesslich wenden wir uns dem Model Checking Problem fu¨r HFL zu, welches wir bereits
invorangegangenenArbeit