@inproceedings{FijalkowKlinPanangaden17,
  author    	= {Nathana{\"{e}}l Fijalkow and
               Bartek Klin and
               Prakash Panangaden},
  title    	= {Expressiveness of Probabilistic Modal Logics, Revisited},
  booktitle	= {ICALP},
  year      	= {2017},
  url       	= {https://doi.org/10.4230/LIPIcs.ICALP.2017.105},
  doi       	= {10.4230/LIPIcs.ICALP.2017.105},
  url_Link      = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7368},
  url_Slides    = {Talk/ICALP_Bisimulation},
  url_Abstract  = {Labelled Markov processes are probabilistic versions of labelled
  transition systems.  In general, the state space of a labelled Markov
  process may be a continuum.  Logical characterizations of probabilistic
  bisimulation and simulation were given by Desharnais et al.  These
  results hold for systems defined on analytic state spaces and
  assume that there are countably many labels in the case of bisimulation
  and finitely many labels in the case of simulation.
<br/>
  In this paper, we first revisit these results by giving simpler and more
  streamlined proofs.  In particular, our proof for simulation has the same
  structure as the one for bisimulation, relying on a new result of a
  topological nature.  This departs from the known proof
  for this result, which uses domain theory techniques and falls out of a
  theory of approximation of Labelled Markov processes.
<br/>
  Both our proofs assume the presence of countably many labels.  We
  investigate the necessity of this assumption, and show that the
  logical characterization of bisimulation may fail when there are
  uncountably many labels.  However, with a stronger assumption on the
  transition functions (continuity instead of just measurability), we can
  regain the logical characterization result, for arbitrarily many labels.
  These new results arose from a new game-theoretic way of understanding
  probabilistic simulation and bisimulation.},
}

{"_id":"kKBSw3PRanQL8ADsr","bibbaseid":"fijalkow-klin-panangaden-expressivenessofprobabilisticmodallogicsrevisited-2017","downloads":0,"creationDate":"2017-11-28T18:01:09.118Z","title":"Expressiveness of Probabilistic Modal Logics, Revisited","author_short":["Fijalkow, N.","Klin, B.","Panangaden, P."],"year":2017,"bibtype":"inproceedings","biburl":"https://nathanael-fijalkow.github.io/perso.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Nathanaël"],"propositions":[],"lastnames":["Fijalkow"],"suffixes":[]},{"firstnames":["Bartek"],"propositions":[],"lastnames":["Klin"],"suffixes":[]},{"firstnames":["Prakash"],"propositions":[],"lastnames":["Panangaden"],"suffixes":[]}],"title":"Expressiveness of Probabilistic Modal Logics, Revisited","booktitle":"ICALP","year":"2017","url":"https://doi.org/10.4230/LIPIcs.ICALP.2017.105","doi":"10.4230/LIPIcs.ICALP.2017.105","url_link":"http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7368","url_slides":"Talk/ICALP_Bisimulation","url_abstract":"Labelled Markov processes are probabilistic versions of labelled transition systems. In general, the state space of a labelled Markov process may be a continuum. Logical characterizations of probabilistic bisimulation and simulation were given by Desharnais et al. These results hold for systems defined on analytic state spaces and assume that there are countably many labels in the case of bisimulation and finitely many labels in the case of simulation. <br/> In this paper, we first revisit these results by giving simpler and more streamlined proofs. In particular, our proof for simulation has the same structure as the one for bisimulation, relying on a new result of a topological nature. This departs from the known proof for this result, which uses domain theory techniques and falls out of a theory of approximation of Labelled Markov processes. <br/> Both our proofs assume the presence of countably many labels. We investigate the necessity of this assumption, and show that the logical characterization of bisimulation may fail when there are uncountably many labels. However, with a stronger assumption on the transition functions (continuity instead of just measurability), we can regain the logical characterization result, for arbitrarily many labels. These new results arose from a new game-theoretic way of understanding probabilistic simulation and bisimulation.","bibtex":"@inproceedings{FijalkowKlinPanangaden17,\n author \t= {Nathana{\\\"{e}}l Fijalkow and\n Bartek Klin and\n Prakash Panangaden},\n title \t= {Expressiveness of Probabilistic Modal Logics, Revisited},\n booktitle\t= {ICALP},\n year \t= {2017},\n url \t= {https://doi.org/10.4230/LIPIcs.ICALP.2017.105},\n doi \t= {10.4230/LIPIcs.ICALP.2017.105},\n url_Link = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7368},\n url_Slides = {Talk/ICALP_Bisimulation},\n url_Abstract = {Labelled Markov processes are probabilistic versions of labelled\n transition systems. In general, the state space of a labelled Markov\n process may be a continuum. Logical characterizations of probabilistic\n bisimulation and simulation were given by Desharnais et al. These\n results hold for systems defined on analytic state spaces and\n assume that there are countably many labels in the case of bisimulation\n and finitely many labels in the case of simulation.\n<br/>\n In this paper, we first revisit these results by giving simpler and more\n streamlined proofs. In particular, our proof for simulation has the same\n structure as the one for bisimulation, relying on a new result of a\n topological nature. This departs from the known proof\n for this result, which uses domain theory techniques and falls out of a\n theory of approximation of Labelled Markov processes.\n<br/>\n Both our proofs assume the presence of countably many labels. We\n investigate the necessity of this assumption, and show that the\n logical characterization of bisimulation may fail when there are\n uncountably many labels. However, with a stronger assumption on the\n transition functions (continuity instead of just measurability), we can\n regain the logical characterization result, for arbitrarily many labels.\n These new results arose from a new game-theoretic way of understanding\n probabilistic simulation and bisimulation.},\n}\n\n","author_short":["Fijalkow, N.","Klin, B.","Panangaden, P."],"key":"FijalkowKlinPanangaden17","id":"FijalkowKlinPanangaden17","bibbaseid":"fijalkow-klin-panangaden-expressivenessofprobabilisticmodallogicsrevisited-2017","role":"author","urls":{"Paper":"https://doi.org/10.4230/LIPIcs.ICALP.2017.105"," link":"http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7368"," slides":"https://nathanael-fijalkow.github.io/Talk/ICALP_Bisimulation"," abstract":"https://nathanael-fijalkow.github.io/Labelled%20Markov%20processes%20are%20probabilistic%20versions%20of%20labelled%20transition%20systems.%20In%20general,%20the%20state%20space%20of%20a%20labelled%20Markov%20process%20may%20be%20a%20continuum.%20Logical%20characterizations%20of%20probabilistic%20bisimulation%20and%20simulation%20were%20given%20by%20Desharnais%20et%20al.%20These%20results%20hold%20for%20systems%20defined%20on%20analytic%20state%20spaces%20and%20assume%20that%20there%20are%20countably%20many%20labels%20in%20the%20case%20of%20bisimulation%20and%20finitely%20many%20labels%20in%20the%20case%20of%20simulation.%20%3Cbr/%3E%20In%20this%20paper,%20we%20first%20revisit%20these%20results%20by%20giving%20simpler%20and%20more%20streamlined%20proofs.%20In%20particular,%20our%20proof%20for%20simulation%20has%20the%20same%20structure%20as%20the%20one%20for%20bisimulation,%20relying%20on%20a%20new%20result%20of%20a%20topological%20nature.%20This%20departs%20from%20the%20known%20proof%20for%20this%20result,%20which%20uses%20domain%20theory%20techniques%20and%20falls%20out%20of%20a%20theory%20of%20approximation%20of%20Labelled%20Markov%20processes.%20%3Cbr/%3E%20Both%20our%20proofs%20assume%20the%20presence%20of%20countably%20many%20labels.%20We%20investigate%20the%20necessity%20of%20this%20assumption,%20and%20show%20that%20the%20logical%20characterization%20of%20bisimulation%20may%20fail%20when%20there%20are%20uncountably%20many%20labels.%20However,%20with%20a%20stronger%20assumption%20on%20the%20transition%20functions%20(continuity%20instead%20of%20just%20measurability),%20we%20can%20regain%20the%20logical%20characterization%20result,%20for%20arbitrarily%20many%20labels.%20These%20new%20results%20arose%20from%20a%20new%20game-theoretic%20way%20of%20understanding%20probabilistic%20simulation%20and%20bisimulation."},"downloads":0,"html":""},"search_terms":["expressiveness","probabilistic","modal","logics","revisited","fijalkow","klin","panangaden"],"keywords":[],"authorIDs":["5a1da46565b42fc01800000f"],"dataSources":["BXc4gcZutK5ptXtTF"]}