| Attributes | Values |
|---|
| rdf:type
| |
| Description
| - We consider a class of finite 1.5-player games (Markov decision processes) where the winning objectives are specified in the branching-time temporal logic qPECTL* (an extension of the qualitative PCTL*). We study decidability and complexity of existence of a winning strategy in these games. We identify a fragment of qPECTL* called detPECTL* for which the existence of a winning strategy is decidable in exponential time, and also the winning strategy can be computed in exponential time (if it exists). Consequently we show that every formula of qPECTL* can be translated to a formula of detPECTL* (in exponential time) so that the resulting formula is equivalent to the original one over finite Markov chains. From this we obtain that for the whole qPECTL*, the existence of a winning finite-memory strategy is decidable in double exponential time. An immediate consequence is that the existence of a winning finite-memory strategy is decidable for the qualitative fragment of PCTL* in triple exponential time. We
- We consider a class of finite 1.5-player games (Markov decision processes) where the winning objectives are specified in the branching-time temporal logic qPECTL* (an extension of the qualitative PCTL*). We study decidability and complexity of existence of a winning strategy in these games. We identify a fragment of qPECTL* called detPECTL* for which the existence of a winning strategy is decidable in exponential time, and also the winning strategy can be computed in exponential time (if it exists). Consequently we show that every formula of qPECTL* can be translated to a formula of detPECTL* (in exponential time) so that the resulting formula is equivalent to the original one over finite Markov chains. From this we obtain that for the whole qPECTL*, the existence of a winning finite-memory strategy is decidable in double exponential time. An immediate consequence is that the existence of a winning finite-memory strategy is decidable for the qualitative fragment of PCTL* in triple exponential time. We (en)
- Předmětem zkoumání jsou konečné hry jednoho a půl hráče (Markovovy rozhodovací procesy), ve kterých je vítězná podmínka zadána pomocí formule logiky větvícího času qPECTL*, což je rozšíření kvalitativní PCTL*. Zkoumáme rozhodnutelnost a složitost problému existence vítězné strategie v těchto hrách. Popíšeme fragment detPECTL*, pro který je tento problém rozhodnutelný v exponenciálním čase a také ukážeme, že vítěznou strategii lze nalézt v exponenciálním čase, pokud tato existuje. Navíc ukážeme, že každou formuli qPECTL* lze převést na formuli detPECTL*, která je ekvivalentní na všech konečných Markovových řetězcích. Tím dostaneme rozhodnutelnost problému existence konečněpaměťové strategie pro qPECTL*. Přímým důsledkem je rozhodnutelnost problému existence konečněpaměťové strategie pro qPCTL*. Také ukážeme, že pro qPCTL je stejný problém řešitelný v exponenciálním čase. V závěru článku se zabýváme vyjadřovací silou konečně pamětových strategií vzhledem k formulím logiky qPCTL. (cs)
|
| Title
| - Strategy Synthesis for Markov Decision Processes and Branching-Time Logics
- Strategy Synthesis for Markov Decision Processes and Branching-Time Logics (en)
- Syntéza strategií pro Markovovy rozhodovací procesy a logiky větvícího času (cs)
|
| skos:prefLabel
| - Strategy Synthesis for Markov Decision Processes and Branching-Time Logics
- Strategy Synthesis for Markov Decision Processes and Branching-Time Logics (en)
- Syntéza strategií pro Markovovy rozhodovací procesy a logiky větvícího času (cs)
|
| skos:notation
| - RIV/00216224:14330/07:00022548!RIV08-MSM-14330___
|
| http://linked.open.../vavai/riv/strany
| |
| http://linked.open...avai/riv/aktivita
| |
| http://linked.open...avai/riv/aktivity
| |
| http://linked.open...iv/cisloPeriodika
| |
| http://linked.open...vai/riv/dodaniDat
| |
| http://linked.open...aciTvurceVysledku
| |
| http://linked.open.../riv/druhVysledku
| |
| http://linked.open...iv/duvernostUdaju
| |
| http://linked.open...titaPredkladatele
| |
| http://linked.open...dnocenehoVysledku
| |
| http://linked.open...ai/riv/idVysledku
| - RIV/00216224:14330/07:00022548
|
| http://linked.open...riv/jazykVysledku
| |
| http://linked.open.../riv/klicovaSlova
| - Markov decision processes; branching-time logics (en)
|
| http://linked.open.../riv/klicoveSlovo
| |
| http://linked.open...odStatuVydavatele
| - DE - Spolková republika Německo
|
| http://linked.open...ontrolniKodProRIV
| |
| http://linked.open...i/riv/nazevZdroje
| - Lecture Notes in Computer Science
|
| http://linked.open...in/vavai/riv/obor
| |
| http://linked.open...ichTvurcuVysledku
| |
| http://linked.open...cetTvurcuVysledku
| |
| http://linked.open...vavai/riv/projekt
| |
| http://linked.open...UplatneniVysledku
| |
| http://linked.open...v/svazekPeriodika
| |
| http://linked.open...iv/tvurceVysledku
| - Brázdil, Tomáš
- Forejt, Vojtěch
|
| issn
| |
| number of pages
| |
| http://localhost/t...ganizacniJednotka
| |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)