License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.SynCoP.2015.63
URN: urn:nbn:de:0030-drops-56107
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5610/
Go to the corresponding OASIcs Volume Portal

Tati, Bharath Siva Kumar ; Siegle, Markus

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

pdf-format:
8.pdf (0.7 MB)

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.

BibTeX - Entry

@InProceedings{tati_et_al:OASIcs:2015:5610,
  author =	{Bharath Siva Kumar Tati and Markus Siegle},
  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 =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{{\'E}tienne Andr{\'e} and Goran Frehse},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5610},
  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}
}

Keywords: Markov chains with actions and state labels, Parameter synthesis, Controller synthesis, Probabilistic model checking
Collection: 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)
Issue Date: 2015
Date of publication: 03.12.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI