Reachability in parametric Interval Markov Chains using constraints
| Autor: | Anicet Bart, Benoît Delahaye, Didier Lime, Paulin Fournier, Charlotte Truchet, Eric Monfroy |
|---|---|
| Přispěvatelé: | Département Automatique, Productique et Informatique (IMT Atlantique - DAPI), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Architectures et Logiciels Sûrs (AeLoS), Laboratoire des Sciences du Numérique de Nantes (LS2N), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS), Théorie, Algorithmes et Systèmes en Contraintes (TASC ), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST) |
| Rok vydání: | 2018 |
| Předmět: |
[INFO.INFO-GT]Computer Science [cs]/Computer Science and Game Theory [cs.GT]
General Computer Science Markov chain Computer science 0102 computer and information sciences 02 engineering and technology 01 natural sciences Theoretical Computer Science Formalism (philosophy of mathematics) [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] 010201 computation theory & mathematics Reachability 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Algorithm ComputingMilieux_MISCELLANEOUS Parametric statistics |
| Zdroj: | Theoretical Computer Science Theoretical Computer Science, Elsevier, 2018, 747, pp.48-74. ⟨10.1016/j.tcs.2018.06.016⟩ |
| ISSN: | 0304-3975 1879-2294 |
| DOI: | 10.1016/j.tcs.2018.06.016 |
| Popis: | Parametric Interval Markov Chains (pIMCs) are a specification formalism that extend Markov Chains (MCs) and Interval Markov Chains (IMCs) by taking into account imprecision in the transition probability values: transitions in pIMCs are labelled with parametric intervals of probabilities. In this work, we study the difference between pIMCs and other Markov Chain abstractions models and investigate three semantics for IMCs: once-and-for-all, interval-Markov-decision-process, and at-every-step. In particular, we prove that all three semantics agree on the maximal/minimal reachability probabilities of a given IMC. We then investigate solutions to several parameter synthesis problems in the context of pIMCs – consistency, qualitative reachability and quantitative reachability – that rely on constraint encodings. Finally, we propose a prototype implementation of our constraint encodings with promising results. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect