Where:

Laboratoire Spécification et Vérification

École Normale Supérieure de Cachan

61, avenue du Président Wilson

94235 Cachan CEDEX

http://www.lsv.ens-cachan.fr

Title:

Quantitative versus probabilistic logics

Description:

 
Formal methods for specifying and verifying qualitative as well as probabilistic properties of critical systems are already well-developed. But other quantitative properties of systems are of interest, e.g., energy consumption, waiting time, various kinds of costs or rewards, their probabilistic versions such as expected rewards, ...

Weighted automata provide a very general framework for the modelization of quantitative systems but a strong theory for specifying and verifying quantitative properties still needs to be developed. In 2005, Droste and Gastin [4] introduced a quantitative (weighted) extension of MSO logic and established its relationship with weighted automata. This result has been generalized to numerous settings such as trees, pictures, concurrent systems, ..., but weighted extensions of temporal logics (linear time or branching time) were lacking. Moreover, weighted MSO was incomparable with the well-established probabilistic versions of CTL or CTL^*.

Very recently, Bollig and Gastin [2] generalized weighted MSO (wMSO) and introduced weighted extensions of CTL and CTL^* which subsume the probabilistic versions of CTL and CTL^*. They reconciled weighted and probabilistic logics by proving that probabilistic or weighted CTL are fragments of wMSO. Several problems were left open and we propose to study some of them during the internship:

1. Satisfiability is undecidable for wMSO in general. Try to identify decidable fragments.
   
   
2. Model checking algorithms are known for probabilistic CTL or CTL^* (see [1, 3]). Try to extend these methods do wCTL or wCTL^* in order to verify other quantitative properties of systems.
   
   
3. Extend the result in [2] with a translation of wCTL^* in wMSO which is valid for probabilistic systems.
   
   
4. Generalize the above results to the expectation semiring defined in [5] which allows to compute expected rewards.

Contact:

 

Benedikt Bollig, Paul Gastin et Marc Zeitoun

Tél: 01 47 40 - 75 38/75 60/77 87

Email: (bollig|gastin|mz)@lsv.ens-cachan.fr

Web: http://www.lsv.ens-cachan.fr/~(bollig|gastin|zeitoun)

References

[1]

B. Bollig and M. Leucker. Verifying qualitative properties of probabilistic programs. In Validation of Stochastic Systems, volume 2925 of Lecture Notes in Computer Science, pages 124–146. Springer, 2004.

[2]

B. Bollig and P. Gastin. Weighted versus Probabilistic Logics. In Proceedings of the 13th International Conference on Developments in Language Theory (DLT'09), volume 5583 of Lecture Notes in Computer Science, pages 18–38. Springer, 2009.

[3]

P. Buchholz and P. Kemper. Model checking for a class of weighted automata. Discrete Event Dynamic Systems, 2009. to appear.

[4]

M. Droste and P. Gastin. Weighted automata and weighted logics. Theoretical Computer Science, 380(1-2):69–86, 2007. Special issue of ICALP'05.

[5]

J. Eisner. Expectation semirings: Flexible EM for learning finite-state transducers. In Proceedings of the ESSLLI workshop on finite-state methods in NLP, 2001.

This document was translated from L^AT_EX by H^EV^EA.