Parameter Synthesis for Parametric Interval Markov Chains - LINA-AELOS Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2015

Parameter Synthesis for Parametric Interval Markov Chains

Résumé

Interval Markov Chains (IMCs) are the base of a classic probabilistic specification theory introduced by Larsen and Jonsson in 1991. They are also a popular abstraction for probabilistic systems. In this paper we study parameter synthesis for a parametric extension of Interval Markov Chains in which the endpoints of intervals may be replaced with parameters. In particular, we propose constructions for the synthesis of all parameter values ensuring several properties such as consistency and consistent reachability in both the existential and universal settings with respect to implementations. We also discuss how our constructions can be modified in order to synthesise all parameter values ensuring other typical properties.
Fichier principal
Vignette du fichier
main.pdf (391.99 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01219823 , version 1 (23-10-2015)

Identifiants

  • HAL Id : hal-01219823 , version 1

Citer

Benoit Delahaye, Didier Lime, Laure Petrucci. Parameter Synthesis for Parametric Interval Markov Chains. [Research Report] LINA-University of Nantes; Ecole Centrale de Nantes (ECN); LIPN. 2015. ⟨hal-01219823⟩
313 Consultations
275 Téléchargements

Partager

Gmail Facebook X LinkedIn More