Using Temporal Logic to Analyse Temporal Logic:
A Hierarchical Approach Based on Intervals
Speaker: Ben Moszkowski (Software Technology Research Laboratory, de Montfort University, Leicester, UK)
Time: 1:30 PM
Date: June, 8th
Place: Solvay room, NO building, 5th floor
Abstract:
Temporal logic has been extensively utilized in academia and industry to
formally specify and verify behavioural properties of numerous kinds of
hardware and software. We present a novel way to apply temporal logic to
the study of a version of itself, namely, propositional linear-time temporal
logic (PTL). This involves a hierarchical framework for obtaining standard
results for PTL, including a small model property, decision procedures and
axiomatic completeness. A large number of the steps involved are expressed
in a propositional version of Interval Temporal Logic (ITL) which is
referred to as PITL. It is a natural generalization of PTL and includes
operators for reasoning about periods of time and sequential composition.
Versions of PTL with finite time and infinite time are both considered and
one benefit of the framework is the ability to systematically reduce
infinite-time reasoning to finite-time reasoning. The treatment of PTL with
the operator Until and past time naturally reduces to that for PTL without
either one. The interval-oriented methodology differs from other analyses
of PTL which typically use sets of formulas and sequences of such sets for
canonical models. Instead we represent models as time intervals expressible
in PITL. The analysis furthermore relates larger intervals with smaller
ones. Being an interval-based formalism, PITL is well suited for
sequentially combining and decomposing the relevant formulas. Consequently,
we can articulate issues of equal significance in more conventional analyses
of PTL but normally only considered at the metalevel. A good example of
this is the existence of bounded models with periodic suffixes for PTL
formulas which are satisfiable in infinite time. We also describe decision
procedures based on binary decision diagrams and exploit some links with
finite-state automata.
Beyond the specific issues involving PTL, the research is a significant
application of ITL and interval-based reasoning and illustrates a general
approach to formally reasoning about sequential and parallel behaviour in
discrete linear time. The work also includes some interesting
representation theorems. In addition, it has relevance to hardware
description and verification since the specification languages PSL/Sugar
(IEEE Standard 1850) and 'temporal e' (part of IEEE Standard 1647) both
contain temporal constructs concerning intervals of time as does the related
SystemVerilog Assertion language contained in SystemVerilog (IEEE Standard
1800), an extension of the IEEE 1364-2001 Verilog language.
FNRS Contact Group Meeting on Synthesis and Verification
Date: October, 18th
Place: ULB, Campus plaine, building NO, level 9, local NO9.06
The program of the day is given hereunder. Those who want to
participate to the meeting must send before friday october 13 an email
to : Jean-François Raskin (jraskin@ulb.ac.be) with subject : « FNRS
day registration ». The lunch will be offered only to those that are
registered.
9h20 : Welcome.
9h30-10h15 : Bernard Lambeau et Christophe Damas (UCL) Scenarios,
Goals, and State Machines : a Win-Win Partnership for Model Synthesis
10h15-10h45 : Coffee Break
10h45-11h45 : Invited talk : Nicolas Markey (LSV - ENS de Cachan)
Verification of Multi-Agent Systems with ATL . Abstract :
Alternating-time Temporal Logic (ATL) is an extension of the well-
known branching-time logic CTL geared towards the specification and
verification of strategic abilities of (coalitions of ) agents to
enforce some ob jective. During this talk, I will introduce the
framework of multi-agent systems, and present some results on the
expressiveness and complexity of ATL.
11h45-14h: Lunch break
14h-14h45 : Michel Sintzoff (UCL) Symbolic generation of optimal
discrete systems
14h45-15h30 : Martin De Wulf (ULB) A Lattice Theory for Solving
Games of Imperfect Information
15h30-16h : Coffee break
16h-16h45 : Gilles Geeraerts (ULB) An efficient algorithm to
compute the coverability set of Petri nets
16h45-17h30 : Axel Legay (ULg) Handling liveness properties in
(omega)-regular model checking
Monitoring and Fault Diagnosis for Real-Time Systems
Abstract: In this talk we review the fundamental results
for the monitoring and fault diagnosis problems for
finite state systems and timed systems. We also address
the following more advanced topics: optimal monitoring and
fault diagnosis for finite state systems and fault diagnosis
for timed systems using digital clocks. We conclude with some
open problems and directions for future work.
UPPAAL Tiga -- Controller Synthesis for Real-Time Systems
Abstract:
UPPAAL Tiga is a recent branch of the real-time verification
tool UPPAAL allowing control programs to be synthesized from timed
game automata models with respect to control purposes specified as CTL
formulas. Thus both safety and reachability games are supported. The
talk will present the efficient on-the-fly algorithm used for
synthesizing winning strategies for timed games, emphasizing recent
methods used for achieving signicant improvement of performance
compared with the first implementation (CONCUR05). UPPAAL Tiga allows
for winning strategies to be represented as BDD/CDDs useful for
compact embedded control programs. In the talk we also show how
UPPAAL Tiga itself may be used for checking refinements between timed
games (useful in settings of partial observability) and how the
on-the-fly algorithm UPPAAL-Tiga may be used (and extended) to
generate testing strategies for real-time systems.
Subexponential algorithms for solving parity games
Place: Plaine campus, NO building, 5th floor, room 2NO5.06
Abstract:
Deciding the winner in a parity game is polynomial time equivalent to
checking if a formula of the modal logic with fixpoint operators (aka.
the modal mu-calculus) holds in a state of a Kripke structure. The exact
computational complexity of the problem is an intriguing open problem:
it is known to be in UP (unambiguous NP) and co-UP, but no polynomial
time algorithm is known. This talk surveys a few recent algorithmic
ideas which yield improved running time bounds for the problem. One is
obtained by a reduction of parity games to the problem of finding the
unique sink in a "unique sink orientation" of a hypercube and it
yields a subexponential randomized algorithm. The other is a
modification of a classical recursive algorithm for solving parity games
that originates from the work of McNaughton and Zielonka and it yields a
subexponential deterministic algorithm.
Monitoring and Fault-Diagnosis with Digital Clocks
Place: Plaine campus, NO building, 5th floor, room 2NO5.06
Abstract:
We study the monitoring and fault-diagnosis problems for dense-time real-time systems,
where observers (monitors and diagnosers) have access to digital rather than analog
clocks. We show how, given a specification modeled as a timed automaton and a timed
automaton model of the digital clock, a sound and optimal (i.e., as precise as possible)
digital-clock monitor can be synthesized. We also show how, given plant and digital clock
modeled as timed automata, we can check for the existence of a digital-clock diagnoser and,
if one exists, how to synthesize it. Finally, we consider the problem of existence of
a digital-clock such that a there is a digital-clock diagnoser.
Abstract:
Stochastic timed systems and stochastic temporal logics have been
proposed to express and check requiremnts like correctness,
availability, survivability or performability of trustworthy
real-time system designs. They are partially accompanied by
model-checking algorithms which can be applied to certify these
requirements on a component level.
This talk gives an overview of recent achievements in this area. It
will detail the achieved results in two related areas: After
introducing the mathematical background and context, I will
report on our efforts to link an industrial modelling tool to academic
state-of-the-art model-checking algorithms. In a nutshell, we enable
timed reachability analysis of uniform continuous-time Markov decision
processes, which are generated from STATEMATE models. We give a
detailed explanation of several construction, transformation,
reduction, and analysis steps required to make this possible.
With a slightly broader perspective, I am then going to introduce
MoDeST (MOdeling and DEscription language for Stochastic Timed
systems), a formalism to support (i) the compositional description of
reactive systems' behavior while covering both (ii) functional and
(iii) nonfunctional system aspects such as timing and
quality-of-service constraints in a single compositional
specification. This unique expressiveness has been exploited in three
recent industrial case studies of rather different nature, ranging
from (i) schedule synthesis and evaluation for a lacquer production
plant, to (ii) energy efficiency assesment of ZigBee devices, and to
(iii) dependability assessment of an emerging standard for future
high-speed cross-European trains.
Development of Safe and Efficient Programs
using Abstract Interpretation
and the CiaoPP System
Speaker: Manuel Hermenegildo (Technical University of Madrid
and University of New Mexico, Spain)
Date: May, 11th
Place: OF2070
Abstract:
One of the fundamental challenges in program development, from large
applications to embedded code, is to be able to develop, in the
shortest time possible, programs that are efficient and correct. We
argue that in order to achieve this goal, in addition to factors such
as better programming languages, substantially improved functionality
is needed from programming environments. We present a novel program
development framework which uses "Abstract Interpretation" as a
fundamental component. Abstract interpretation is a technique which
has allowed the development of very sophisticated program analyzers
and transformers, which are at the same time provably correct and
highly practical. The framework that we present uses this type of
program analysis to obtain information about the program. This
information is then used to validate programs with respect to partial
specifications written using assertions, to detect and locate bugs, to
simplify run-time tests, to perform high-level program transformations
(such as specialization, parallelization, or resource usage control),
and to enrich mobile code with safety certificates. The system can
reason with much richer information than, for example, traditional
type declarations. This includes pointer aliasing, shapes,
exceptions, determinacy, abounds on resource consumption (such as
computational cost or sizes of data in the program), etc. CiaoPP, the
preprocessor of the Ciao multi-paradigm programming system is an
implementation of this framework and will be used to illustrate these
ideas.