DROPS

Document

DOI: 10.4230/OASIcs.SynCoP.2015.63

Parameter and Controller Synthesis for Markov Chains with Actions and State Labels

Authors: Bharath Siva Kumar Tati and Markus Siegle

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract

This paper introduces a novel approach for synthesizing parameters and controllers for Markov Chains with Actions and State Labels (ASMC). Requirements which are to be met by the controlled system are specified as formulas of asCSL, which is a powerful temporal logic for characterizing both state properties and action sequences of a labeled Markov chain. The paper proposes two separate - but related - algorithms for untimed until type and untimed general asCSL formulas. In the former case, a set of transition rates and a common rate reduction factor are determined. In the latter case, a controller which is to be composed in parallel with the given ASMC is synthesized. Both algorithms are based on some rather simple heuristics.

Cite as

Bharath Siva Kumar Tati and Markus Siegle. Parameter and Controller Synthesis for Markov Chains with Actions and State Labels. In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 63-76, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{tati_et_al:OASIcs.SynCoP.2015.63,
  author =	{Tati, Bharath Siva Kumar and Siegle, Markus},
  title =	{{Parameter and Controller Synthesis for Markov Chains with Actions and State Labels}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{63--76},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.63},
  URN =		{urn:nbn:de:0030-drops-56107},
  doi =		{10.4230/OASIcs.SynCoP.2015.63},
  annote =	{Keywords: Markov chains with actions and state labels, Parameter synthesis, Controller synthesis, Probabilistic model checking}
}

Search Results

Documents authored by Tati, Bharath Siva Kumar

Parameter and Controller Synthesis for Markov Chains with Actions and State Labels

Abstract

Cite as

Thanks for your feedback!

Could not send message