Verification of Non-Regular Program Properties

Most temporal logics which have been introduced and studied in the
past decades can be embedded into the modal mu-calculus. 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 enriches
the mu-calculus with a sequential composition operator and thereby
allows to characterise context-free processes. The Modal Iteration
Calculus uses inflationary fixpoints to exceed the expressive power
of the mu-calculus. Higher-Order Fixpoint Logic (HFL) incorporates
a simply typed lambda-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 decision
problems. For instance are the satisfiability problems for the
above mentioned logics undecidable. We investigate in this work the
model checking problem of three different logics 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-operator is 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 k-EXPTIME-complete for HFL(k), the
fragment of HFL obtained by restricting functions in the
lambda-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, we show how HFL can be used as a
tool for the development of algorithms. Its high expressivity
allows to encode a wide variety of problems as instances of model
checking 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 compare
them with respect to expressive power.