Temporal logics

Researches on Temporal Logics,
Automata, and Games
Angelo Montanari
Departement of Mathematics and Computer
Science, University of Udine
Udine, May 8, 2008
Research topic: temporal
logics (TL) - 1

Temporal logics for time granularity:
- metric temporal logics, axiomatic systems for metric temporal
logics, executability
- classical/non classical logics for time granularity, definability issues,
axiomatic systems, decidability of the theories of finite, upward
unbounded, and downward unbounded layered structures
- combined temporal logics, model checking procedures for combined
temporal logics, implementation
- applications (formal specifications, temporal databases,
bioinformatics)
Research topic: temporal
logics (TL) - 2

Interval temporal logics:
- expressiveness, axiomatic systems
- decidability/undecidability results
- proof methods for interval temporal logics, tableau systems,
implementation
- applications (artificial intelligence, temporal databases,
bioinformatics)
Research topic: automata
theory (AT)

Automata theory:
- combined automata for time granularity
- single-string automata, restricted labeled automata, ultimately
periodic automata, implementation
- automaton-based solution to the model checking problem for
monadic second-order logic over (deterministic) colored trees
(contraction method)
- on the relationships between the contraction method and Shelah’s
composition method
Research topic: game theory
(GT) - 1

Game theory:
- comparison games (bisimulation games) as a method to
measure the expressive power of a (temporal) logic/to
compare the expressive power of different (temporal)
logics
- comparison games (first-order Ehrenfeucht-Fraissé
games) as a tool to compare structures and determine
where and how they differ (remoteness)
Research topic: game theory
(GT) - 2
- algorithmic game theory: efficient algorithms (taking advantage of
generalized suffix trees) for computing the remoteness and the sets of
optimal moves for both players in the case of labelled successor
structures (recently extended to structures with a bounded ordering
relation), implementation
- applications: bioinformatics (e.g., to compare genome assemblies
of the same organism obtained by different programs--a left-to-right
comparison is not adequate, because different parts may be ordered
differently and some other segments may not be related)
Research topic: spatiotemporal databases (DB)

A development framework for spatio-temporal databases:
- conceptual design (spatio-temporal conceptual models and
software tools for their visual synthesis)
- logical design 1: translation into temporally-extended spatial
relational schemas, implementation
- logical design 2: translation into XML Schema document,
implementation

Temporal databases for the life sciences
People
Temporal logics:
Maarten de Rijke, Adriano Peron, Alberto Policriti, Valentin Goranko,
Agostino Dovier, Carla Piazza, Massimo Franceschet, Guido
Sciavicco, Nicola Vitacolonna, Gabriele Puppis, Davide Bresolin,
Elisabetta De Maria, Pietro Sala, Dario Della Monica
Automata theory:
Ugo Dal Lago, Massimo Franceschet, Gabriele Puppis
Game theory:
Alberto Policriti, Valentin Goranko, Nicola Vitacolonna, Elisabetta De
Maria
Spatio-temporal databases:
Carlo Combi, Emiliano Dalla, Donatella Gubiani, Massimo
Franceschet, Giuseppe Pozzi, Marco Zantoni
PhD students - 1
Massimo Franceschet (PhD 2002)
PhD thesis: “Dividing and Conquering the Layered Land” (TL)
during his PhD, he visited prof. Maarten de Rijke at the CWI, University
of Amsterdam (NL)
assistant professor at the University of Chieti-Pescara (2002-2006)
assistant professor at the University of Udine (2006-)
Guido Sciavicco (PhD 2004)
PhD thesis: “Adventures in Propositional Interval Temporal Logics” (TL)
during his PhD, he visited prof. Valentin Goranko at the Rand Afrikaans
University of Johannesburg, South Africa
post-doc at the University of Murcia, Espana (2005-)
PhD students - 2
Nicola Vitacolonna (PhD 2005)
PhD thesis: “Intervals: logics, algorithms, and games” (GT)
post-doc at the University of Udine (2005-2007)
assistant professor at the University of Udine (2007-)
Gabriele Puppis (PhD 2006)
PhD thesis: “Automata for branching and layered structures” (AT)
during his PhD, he visited prof. Wolfgang Thomas at the University of
Aachen, Germany
E.W. Beth Dissertation Prize 2006 award for the Ph.D. thesis granted by
the "Association of Logic, Language, and Information – FoLLI”
post-doc at the University of Udine, Italy (2006-)
PhD students - 3
Davide Bresolin (PhD 2007)
PhD thesis: “Proof methods for interval temporal logics” (TL)
during his PhD, he visited prof. Ewa Orlowska at the University of
Warsaw and prof. Valentin Goranko at the University of Witwatersrand,
Johannesburg, South Africa
post-doc at the University of Verona, Italy (2007-)
Donatella Gubiani (PhD 2008)
PhD thesis: “ChronoGeoGraph: a Development Framework for SpatioTemporal Databases” (DB), University of Chieti-Pescara
during her PhD, she visited prof. Stefano Spaccapietra at the Swiss
Federal Institute of Technology
Current PhD students
Elisabetta De Maria (2006-2008)
Topics: application of formal methods to bioinformatics, including model
checking and game theory (GT)
during her PhD, she visited prof. Francois Fages at INRIA Rocquencourt,
Paris, France
Pietro Sala (2007-2009)
Topics: decidability/undecidability of interval temporal logics, proof
methods, implementation (TL)
Dario Della Monica (2008-2010)
Topics: decidability/undecidability of interval temporal logics, proof
methods, implementation (TL)
Research projects (2005-) - 1



TL: PRIN project on “Vincoli e preferenze come formalismo unificante
per l’analisi di sistemi informatici e la soluzione di problemi reali”, with
Francesca Rossi et al. (2006/08)
DB: FIRB project on “Il riconoscimento molecolare nelle interazioni
proteina-ligando, proteina-proteina e proteina-superficie: sviluppo di
approcci sperimentali e computazionali integrati per lo studio di
sistemi di interesse farmaceutico”, with Hugo Monaco et al. (2006/08)
TL: NWO project on “Model checking methods and tools for hybrid
logics, with Holger Schlingloff et al. (2002/06)
Research projects (2005-) - 2



TL: INTAS project on “Algebraic and deduction methods in non
classical logics and their applications to computer science”, with
Alberto Policriti et al. (2005/07)
TL: GNCS project on “Sviluppo di risolutori con vincoli e loro
applicazione in teoria dei codici e bioinformatica”, with Agostino
Dovier et al. (2005)
TL/DB: Friuli Venezia Giulia project on “BIOCHECK: uno strumento
per la simulazione e verifica di sistemi biologici”, with Alberto Policriti
(2006/07)
Research projects (2005-) - 3





TL: Italy-South Africa bilateral projects on temporal logics in
computer and information sciences, with Valentin Goranko et al.
(2005/07)
GT/AT: Research Networking Programme “Games for Design and
Verification (GAMES)”, with Erich Graedel et al. (2008-2013)
TL: Italy-Spain bilateral project on formal methods for interval
temporal logics, with Roque Marin and Guido Sciavicco (proposal)
AT: Italy-France bilateral projects on automaton-based methods for
the verification of infinite state systems, with Didier Caucal and
Thomas Colcombet (proposals)
TL/DB: FP 7 project on “Bio-Abstractor: Intelligent, Multi-Granular
Structured Digital Abstracts for Biomedicine”, with Udo Hahn et al.
(proposal)