Qualitative Analysis of VASS-Induced MDPs

Parosh Aziz Abdulla; Radu Ciobanu; Richard Mayr; Arnaud Sangnier; Jeremy Sproston

doi:10.1007/978-3-662-49630-5_19

Qualitative Analysis of VASS-Induced MDPs

Parosh Aziz Abdulla, Radu Ciobanu, Richard Mayr, Arnaud Sangnier, Jeremy Sproston

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We consider infinite-state Markov decision processes (MDPs) that are induced by extensions of vector addition systems with states (VASS). Verification conditions for these MDPs are described by reachability and Buchi objectives w.r.t. given sets of control-states. We study the decidability of some qualitative versions of these objectives, i.e., the decidability of whether such objectives can be achieved surely, almost-surely, or limit-surely. While most such problems are undecidable in general, some are decidable for large subclasses in which either only the controller or only the random environment can change the counter values (while the other side can only change control-states).

Original language	English
Title of host publication	Foundations of Software Science and Computation Structures
Subtitle of host publication	19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings
Publisher	Springer Berlin Heidelberg
Pages	319-334
Number of pages	16
ISBN (Electronic)	978-3-662-49630-5
ISBN (Print)	978-3-662-49629-9
DOIs	https://doi.org/10.1007/978-3-662-49630-5_19
Publication status	Published - Mar 2016
Event	FOSSACS - Eindhoven, Netherlands Duration: 2 Apr 2016 → 8 Apr 2016

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	9634
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	FOSSACS
Country/Territory	Netherlands
City	Eindhoven
Period	2/04/16 → 8/04/16

Access to Document

10.1007/978-3-662-49630-5_19

mainAccepted author manuscript, 469 KBLicence: Creative Commons: Attribution (CC-BY)

http://link.springer.com/chapter/10.1007/978-3-662-49630-5_19

Energy Efficient Control
Mayr, R.
EPSRC
1/09/15 → 31/08/19
Project: Research

Cite this

Abdulla, P. A., Ciobanu, R., Mayr, R., Sangnier, A., & Sproston, J. (2016). Qualitative Analysis of VASS-Induced MDPs. In Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (pp. 319-334). (Lecture Notes in Computer Science; Vol. 9634). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-49630-5_19

Abdulla, Parosh Aziz ; Ciobanu, Radu ; Mayr, Richard et al. / Qualitative Analysis of VASS-Induced MDPs. Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Springer Berlin Heidelberg, 2016. pp. 319-334 (Lecture Notes in Computer Science).

@inproceedings{eb332ccfb97b4c3d85851a2dd642d02c,

title = "Qualitative Analysis of VASS-Induced MDPs",

abstract = "We consider infinite-state Markov decision processes (MDPs) that are induced by extensions of vector addition systems with states (VASS). Verification conditions for these MDPs are described by reachability and Buchi objectives w.r.t. given sets of control-states. We study the decidability of some qualitative versions of these objectives, i.e., the decidability of whether such objectives can be achieved surely, almost-surely, or limit-surely. While most such problems are undecidable in general, some are decidable for large subclasses in which either only the controller or only the random environment can change the counter values (while the other side can only change control-states).",

author = "Abdulla, {Parosh Aziz} and Radu Ciobanu and Richard Mayr and Arnaud Sangnier and Jeremy Sproston",

year = "2016",

month = mar,

doi = "10.1007/978-3-662-49630-5_19",

language = "English",

isbn = "978-3-662-49629-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "319--334",

booktitle = "Foundations of Software Science and Computation Structures",

note = "FOSSACS ; Conference date: 02-04-2016 Through 08-04-2016",

}

Abdulla, PA, Ciobanu, R, Mayr, R, Sangnier, A & Sproston, J 2016, Qualitative Analysis of VASS-Induced MDPs. in Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9634, Springer Berlin Heidelberg, pp. 319-334, FOSSACS, Eindhoven, Netherlands, 2/04/16. https://doi.org/10.1007/978-3-662-49630-5_19

Qualitative Analysis of VASS-Induced MDPs. / Abdulla, Parosh Aziz; Ciobanu, Radu; Mayr, Richard et al.

Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Springer Berlin Heidelberg, 2016. p. 319-334 (Lecture Notes in Computer Science; Vol. 9634).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Qualitative Analysis of VASS-Induced MDPs

AU - Abdulla, Parosh Aziz

AU - Ciobanu, Radu

AU - Mayr, Richard

AU - Sangnier, Arnaud

AU - Sproston, Jeremy

PY - 2016/3

Y1 - 2016/3

N2 - We consider infinite-state Markov decision processes (MDPs) that are induced by extensions of vector addition systems with states (VASS). Verification conditions for these MDPs are described by reachability and Buchi objectives w.r.t. given sets of control-states. We study the decidability of some qualitative versions of these objectives, i.e., the decidability of whether such objectives can be achieved surely, almost-surely, or limit-surely. While most such problems are undecidable in general, some are decidable for large subclasses in which either only the controller or only the random environment can change the counter values (while the other side can only change control-states).

AB - We consider infinite-state Markov decision processes (MDPs) that are induced by extensions of vector addition systems with states (VASS). Verification conditions for these MDPs are described by reachability and Buchi objectives w.r.t. given sets of control-states. We study the decidability of some qualitative versions of these objectives, i.e., the decidability of whether such objectives can be achieved surely, almost-surely, or limit-surely. While most such problems are undecidable in general, some are decidable for large subclasses in which either only the controller or only the random environment can change the counter values (while the other side can only change control-states).

U2 - 10.1007/978-3-662-49630-5_19

DO - 10.1007/978-3-662-49630-5_19

M3 - Conference contribution

SN - 978-3-662-49629-9

T3 - Lecture Notes in Computer Science

SP - 319

EP - 334

BT - Foundations of Software Science and Computation Structures

PB - Springer Berlin Heidelberg

T2 - FOSSACS

Y2 - 2 April 2016 through 8 April 2016

ER -

Abdulla PA, Ciobanu R, Mayr R, Sangnier A, Sproston J. Qualitative Analysis of VASS-Induced MDPs. In Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Springer Berlin Heidelberg. 2016. p. 319-334. (Lecture Notes in Computer Science). doi: 10.1007/978-3-662-49630-5_19

Qualitative Analysis of VASS-Induced MDPs

Abstract

Publication series

Conference

Access to Document

Fingerprint

Projects

Energy Efficient Control

Cite this