Show simple item record

dc.contributor.advisorMayr, Richarden
dc.contributor.advisorEtessami, Koushaen
dc.contributor.authorCiobanu, Raduen
dc.date.accessioned2019-07-25T15:36:25Z
dc.date.available2019-07-25T15:36:25Z
dc.date.issued2019-07-01
dc.identifier.urihttp://hdl.handle.net/1842/35879
dc.description.abstractIn the first part of the thesis, we prove the decidability (and PSPACE-completeness) of the universal safety property on a timed extension of Petri Nets, called Timed Petri Nets. Every token has a real-valued clock (a.k.a. age), and transition firing is constrained by the clock values that have integer bounds (using strict and non-strict inequalities). The newly created tokens can either inherit the age from an input token of the transition or it can be reset to zero. In the second part of the thesis, we refer to systems with controlled behaviour that are probabilistic extensions of VASS and One-Counter Automata. Firstly, we consider infinite state Markov Decision Processes (MDPs) that are induced by probabilistic extensions of VASS, called VASS-MDPs. We show that most of the qualitative problems for general VASS-MDPs are undecidable, and consider a monotone subclass in which only the controller can change the counter values, called 1-VASS-MDPs. In particular, we show that limit-sure control state reachability for 1-VASS-MDPs is decidable, i.e., checking whether one can reach a set of control states with probability arbitrarily close to 1. Unlike for finite state MDPs, the control state reachability property may hold limit surely (i.e. using an infinite family of strategies, each of which achieving the objective with probability ≥ 1-e, for every e > 0), but not almost surely (i.e. with probability 1). Secondly, we consider infinite state MDPs that are induced by probabilistic extensions of One-Counter Automata, called One-Counter Markov Decision Processes (OC-MDPs). We show that the almost-sure {1;2;3}-Parity problem for OC-MDPs is at least as hard as the limit-sure selective termination problem for OC-MDPs, in which one would like to reach a particular set of control states and counter value zero with probability arbitrarily close to 1.en
dc.contributor.sponsorEngineering and Physical Sciences Research Council (EPSRC)en
dc.language.isoen
dc.publisherThe University of Edinburghen
dc.relation.hasversionP. Abdulla, R. Ciobanu, R. Mayr, A. Sangnier, and J. Sproston. Qualitative analysis on VASS-induced MDPs. In International Conference on Foundations of Software Science and Computational Structures (FoSSaCS), volume 9634 of LNCS, pages 319–334. Springer, 2016.en
dc.relation.hasversionP. A. Abdulla, R. Ciobanu, R. Mayr, A. Sangnier, and J. Sproston. Universal safety for timed Petri nets is PSPACE-complete. In International Conference of Concurrency theory (CONCUR). LIPIcs (DOI: 10.4230/LIPIcs.CONCUR.2018.6), 2018.en
dc.subjectformal verificationen
dc.subjectPetri netsen
dc.subjectTimed Petri netsen
dc.subjectVASS-MDPsen
dc.subjectconcurrent computationsen
dc.subjectOne-counter Markov Decision Processesen
dc.subjectOC-MDPsen
dc.titleVerification problems for timed and probabilistic extensions of Petri Netsen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record