Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Tati, Bharath Siva Kumar; Siegle, Markus http://www.dagstuhl.de/oasics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-56107
URL:

;

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

pdf-format:


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
Seminar: 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)
Issue date: 2015
Date of publication: 2015


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