| dc.description.abstract | Parametric and Real-Time Systems play a central role in the theory underlying
the Verification and Synthesis problems.
Real-time systems are present everywhere and are used in safety critical
applications, such as flight controllers. Failures in such systems can be
very expensive and even life threatening and, moreover, they are quite
hard to design and verify. For these reasons, the development of formal
methods for the modeling and analysis of safety-critical systems is
an active area of computer science research.
The standard formalism used to specify the wished behaviour of a realtime
system is temporal logic. Traditional temporal logics, such as linear
temporal logic (LTL), allow only qualitative assertions about the temporal
ordering of events. However, in several circumstances, for assessing the
efficiency of the system being modeled, it may be useful to have additional
quantitative guarantees. An extension of LTL with a real-time semantics
is given by the Metric Interval Temporal Logic (MITL), where changes
of truth values happen according to a splitting of the line of non-negative
reals into intervals.
However, even with quantitative temporal logics, we would actually like
to find out what quantitative bounds can be placed on the logic operators.
In this thesis we face with the above problem proposing a parametric
extension of MITL, that is the parametric metric interval temporal logic
(PMITL), which allows to introduce parameters within intervals . For this
logic, we study decision problems which are the analogous of satisfiability,
validity and model-checking problems for non-parametric temporal
logic. PMITL turns out to be decidable and we show that, when parameter
valuations give only non-singular sets, the considered problems are all
decidable, EXPSPACE-complete, and have the same complexity as in MITL.
Moreover, we investigate the computational complexity of these problems
for natural fragments of PMITL, and show that in meaningful fragments
of the logic they are PSPACE-complete.
We also consider a remarkable problem expressed by queries where the
values that each parameter may assume are either existentially or universally
quantified. We solve this problem in several cases and we propose an
algorithm in EXPSPACE.
Another interesting application of the temporal logic is when it is used
to express specification of concurrent programs, where programs and properties
are formalized as regular languages of infinite words. In this case,
the verification problem (whether the program satisfies the specification)
corresponds to solve the language inclusion problem.
In the second part of this thesis we consider the Synthesis problem for realtime
systems, investigating the applicability of automata constructions that
avoid determinization for solving the language inclusion problem and the
realizability problem for real-time logics. Since Safra’s determinization
procedure is difficult to implement, we present Safraless algorithms for
automata on infinite timed words. [edited by author] | en_US |
