Difference between revisions of "Jobs/M2 2017 MC Spot Generic Acc"

From LRDE

Line 5: Line 5:
 
|Research field=Model checking
 
|Research field=Model checking
 
|Related project=Spot
 
|Related project=Spot
  +
|Advisor=Alexandre Duret-Lutz
 
|General presentation of the field=The Spot library (http://spot.lrde.epita.fr/) contains many algorithms for translating LTL formulas into omega-automata, and to simplify these formulas and automata. It also provides support to build an LTL model checker, through algorithms testing whether the language of such an automaton is empty or not.
 
|General presentation of the field=The Spot library (http://spot.lrde.epita.fr/) contains many algorithms for translating LTL formulas into omega-automata, and to simplify these formulas and automata. It also provides support to build an LTL model checker, through algorithms testing whether the language of such an automaton is empty or not.
   
Line 19: Line 20:
 
|Contact=< adl at lrde.epita.fr >
 
|Contact=< adl at lrde.epita.fr >
 
|Compensation=1000 € gross / month
 
|Compensation=1000 € gross / month
|Future work opportunities=The internship can easily be prolonged as a PhD thesis.
+
|Future work opportunities=The internship can easily be prolonged as a PhD thesis.
 
|Type=Master Internship
 
|Type=Master Internship
 
|Language=en
 
|Language=en

Revision as of 17:41, 30 November 2016

Algorithms for generic acceptance
Reference id

M2 2017 MC Spot Generic Acc

Dates

5-6 months in 2017

Research field

Model checking

Related project

Spot

Advisor

Alexandre Duret-Lutz

General presentation of the field

The Spot library (http://spot.lrde.epita.fr/) contains many algorithms for translating LTL formulas into omega-automata, and to simplify these formulas and automata. It also provides support to build an LTL model checker, through algorithms testing whether the language of such an automaton is empty or not.

Omega-automata are used to represent languages over infinite words. These automata can be defined using numerous acceptance conditions such as Büchi, co-Büchi, Rabin, Streett, Parity, etc. Spot actually supports these acceptances condition in a generic way and allow them to be combined as desired.

Prerequisites

Experience of C++, notions of automata (not necessarily omega-automata).

Objectives

The goal is to implement several algorithms that transform automata using one acceptance condition into automata using another acceptance condition. Some of these conversions are essential to some decision procedures.

For instance, we currently have an implement of Krishnan's algorithm for converting a deterministic Rabin automata into an equivalent deterministic Büchi automaton when such an automaton exist. We believe the procedure could be extended to handle deterministic "Generic Rabin" as input. Implementing such a new transformation would give us an efficient way to decide whether some LTL formula is realizable by a deterministic Büchi automaton, because we can already transform LTL into generic Rabin.

Benefit for the candidate
  • Learning many results about omega-automata (do not be afraid by all these new names!)
  • Contributing on an open-source library and tools used by other researchers on omega-automata
References

Krishnan et al.'s "Deterministic ω-Automata vis-a-vis Deterministic Büchi Automata" (ISAAC'94)

http://spot.lrde.epita.fr/

Place LRDE: How to get to us
Compensation

1000 € gross / month

Future work opportunities

The internship can easily be prolonged as a PhD thesis.

Contact

< adl at lrde.epita.fr > < adl at lrde.epita.fr >