--- _id: '1870' abstract: - lang: eng text: We investigate the problem of checking if a finite-state transducer is robust to uncertainty in its input. Our notion of robustness is based on the analytic notion of Lipschitz continuity - a transducer is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions. We show that K-robustness is undecidable even for deterministic transducers. We identify a class of functional transducers, which admits a polynomial time automata-theoretic decision procedure for K-robustness. This class includes Mealy machines and functional letter-to-letter transducers. We also study K-robustness of nondeterministic transducers. Since a nondeterministic transducer generates a set of output words for each input word, we quantify output perturbation using setsimilarity functions. We show that K-robustness of nondeterministic transducers is undecidable, even for letter-to-letter transducers. We identify a class of set-similarity functions which admit decidable K-robustness of letter-to-letter transducers. alternative_title: - LIPIcs author: - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Jan full_name: Otop, Jan id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87 last_name: Otop - first_name: Roopsha full_name: Samanta, Roopsha id: 3D2AAC08-F248-11E8-B48F-1D18A9856A87 last_name: Samanta citation: ama: 'Henzinger TA, Otop J, Samanta R. Lipschitz robustness of finite-state transducers. In: Leibniz International Proceedings in Informatics, LIPIcs. Vol 29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:431-443. doi:10.4230/LIPIcs.FSTTCS.2014.431' apa: 'Henzinger, T. A., Otop, J., & Samanta, R. (2014). Lipschitz robustness of finite-state transducers. In Leibniz International Proceedings in Informatics, LIPIcs (Vol. 29, pp. 431–443). Delhi, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431' chicago: Henzinger, Thomas A, Jan Otop, and Roopsha Samanta. “Lipschitz Robustness of Finite-State Transducers.” In Leibniz International Proceedings in Informatics, LIPIcs, 29:431–43. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431. ieee: T. A. Henzinger, J. Otop, and R. Samanta, “Lipschitz robustness of finite-state transducers,” in Leibniz International Proceedings in Informatics, LIPIcs, Delhi, India, 2014, vol. 29, pp. 431–443. ista: 'Henzinger TA, Otop J, Samanta R. 2014. Lipschitz robustness of finite-state transducers. Leibniz International Proceedings in Informatics, LIPIcs. FSTTCS: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 29, 431–443.' mla: Henzinger, Thomas A., et al. “Lipschitz Robustness of Finite-State Transducers.” Leibniz International Proceedings in Informatics, LIPIcs, vol. 29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 431–43, doi:10.4230/LIPIcs.FSTTCS.2014.431. short: T.A. Henzinger, J. Otop, R. Samanta, in:, Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 431–443. conference: end_date: 2014-12-17 location: Delhi, India name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science' start_date: 2014-12-15 date_created: 2018-12-11T11:54:27Z date_published: 2014-12-01T00:00:00Z date_updated: 2021-01-12T06:53:45Z day: '01' ddc: - '004' department: - _id: ToHe doi: 10.4230/LIPIcs.FSTTCS.2014.431 file: - access_level: open_access checksum: 7b1aff1710a8bffb7080ec07f62d9a17 content_type: application/pdf creator: system date_created: 2018-12-12T10:09:11Z date_updated: 2020-07-14T12:45:19Z file_id: '4734' file_name: IST-2017-804-v1+1_37.pdf file_size: 562151 relation: main_file file_date_updated: 2020-07-14T12:45:19Z has_accepted_license: '1' intvolume: ' 29' language: - iso: eng month: '12' oa: 1 oa_version: Published Version page: 431 - 443 publication: Leibniz International Proceedings in Informatics, LIPIcs publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '5227' pubrep_id: '804' quality_controlled: '1' status: public title: Lipschitz robustness of finite-state transducers tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 29 year: '2014' ... --- _id: '1875' abstract: - lang: eng text: We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and can ensure the readability of the repaired program using user-defined expression templates; the framework also generates a set of inductive assertions that serve as a proof of correctness of the repaired program. As a step toward integrating programmer intent and intuition in automated program repair, we present a cost-aware formulation - given a cost function associated with permissible statement modifications, the goal is to ensure that the total program modification cost does not exceed a given repair budget. As part of our predicate abstractionbased solution framework, we present a sound and complete algorithm for repair of Boolean programs. We have developed a prototype tool based on SMT solving and used it successfully to repair diverse errors in benchmark C programs. alternative_title: - LNCS author: - first_name: Roopsha full_name: Samanta, Roopsha id: 3D2AAC08-F248-11E8-B48F-1D18A9856A87 last_name: Samanta - first_name: Oswaldo full_name: Olivo, Oswaldo last_name: Olivo - first_name: Emerson full_name: Allen, Emerson last_name: Allen citation: ama: 'Samanta R, Olivo O, Allen E. Cost-aware automatic program repair. In: Müller-Olm M, Seidl H, eds. Vol 8723. Springer; 2014:268-284. doi:10.1007/978-3-319-10936-7_17' apa: 'Samanta, R., Olivo, O., & Allen, E. (2014). Cost-aware automatic program repair. In M. Müller-Olm & H. Seidl (Eds.) (Vol. 8723, pp. 268–284). Presented at the SAS: Static Analysis Symposium, Munich, Germany: Springer. https://doi.org/10.1007/978-3-319-10936-7_17' chicago: Samanta, Roopsha, Oswaldo Olivo, and Emerson Allen. “Cost-Aware Automatic Program Repair.” edited by Markus Müller-Olm and Helmut Seidl, 8723:268–84. Springer, 2014. https://doi.org/10.1007/978-3-319-10936-7_17. ieee: 'R. Samanta, O. Olivo, and E. Allen, “Cost-aware automatic program repair,” presented at the SAS: Static Analysis Symposium, Munich, Germany, 2014, vol. 8723, pp. 268–284.' ista: 'Samanta R, Olivo O, Allen E. 2014. Cost-aware automatic program repair. SAS: Static Analysis Symposium, LNCS, vol. 8723, 268–284.' mla: Samanta, Roopsha, et al. Cost-Aware Automatic Program Repair. Edited by Markus Müller-Olm and Helmut Seidl, vol. 8723, Springer, 2014, pp. 268–84, doi:10.1007/978-3-319-10936-7_17. short: R. Samanta, O. Olivo, E. Allen, in:, M. Müller-Olm, H. Seidl (Eds.), Springer, 2014, pp. 268–284. conference: end_date: 2014-09-14 location: Munich, Germany name: 'SAS: Static Analysis Symposium' start_date: 2014-09-11 date_created: 2018-12-11T11:54:29Z date_published: 2014-09-01T00:00:00Z date_updated: 2021-01-12T06:53:46Z day: '01' ddc: - '000' - '005' department: - _id: ToHe doi: 10.1007/978-3-319-10936-7_17 editor: - first_name: Markus full_name: Müller-Olm, Markus last_name: Müller-Olm - first_name: Helmut full_name: Seidl, Helmut last_name: Seidl file: - access_level: open_access checksum: 78ec4ea1bdecc676cd3e8cad35c6182c content_type: application/pdf creator: system date_created: 2018-12-12T10:07:51Z date_updated: 2020-07-14T12:45:19Z file_id: '4650' file_name: IST-2014-313-v1+1_SOE.SAS14.pdf file_size: 409485 relation: main_file file_date_updated: 2020-07-14T12:45:19Z has_accepted_license: '1' intvolume: ' 8723' language: - iso: eng month: '09' oa: 1 oa_version: Submitted Version page: 268 - 284 publication_status: published publisher: Springer publist_id: '5221' pubrep_id: '313' quality_controlled: '1' scopus_import: 1 status: public title: Cost-aware automatic program repair type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 8723 year: '2014' ... --- _id: '2027' abstract: - lang: eng text: We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties inMDPs. In contrast with other related techniques, our approach is not restricted to time-bounded (finite-horizon) or discounted properties, nor does it assume any particular properties of the MDP. We also show how our methods extend to LTL objectives. We present experimental results showing the performance of our framework on several examples. acknowledgement: This research was funded in part by the European Research Council (ERC) under grant agreement 246967 (VERIWARE), by the EU FP7 project HIERATIC, by the Czech Science Foundation grant No P202/12/P612, by EPSRC project EP/K038575/1. alternative_title: - LNCS author: - first_name: Tomáš full_name: Brázdil, Tomáš last_name: Brázdil - first_name: Krishnendu full_name: Chatterjee, Krishnendu id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87 last_name: Chatterjee orcid: 0000-0002-4561-241X - first_name: Martin full_name: Chmelik, Martin id: 3624234E-F248-11E8-B48F-1D18A9856A87 last_name: Chmelik - first_name: Vojtěch full_name: Forejt, Vojtěch last_name: Forejt - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 - first_name: Marta full_name: Kwiatkowska, Marta last_name: Kwiatkowska - first_name: David full_name: Parker, David last_name: Parker - first_name: Mateusz full_name: Ujma, Mateusz last_name: Ujma citation: ama: 'Brázdil T, Chatterjee K, Chmelik M, et al. Verification of markov decision processes using learning algorithms. In: Cassez F, Raskin J-F, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8837. Society of Industrial and Applied Mathematics; 2014:98-114. doi:10.1007/978-3-319-11936-6_8' apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretinsky, J., Kwiatkowska, M., … Ujma, M. (2014). Verification of markov decision processes using learning algorithms. In F. Cassez & J.-F. Raskin (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8837, pp. 98–114). Sydney, Australia: Society of Industrial and Applied Mathematics. https://doi.org/10.1007/978-3-319-11936-6_8' chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Kretinsky, Marta Kwiatkowska, David Parker, and Mateusz Ujma. “Verification of Markov Decision Processes Using Learning Algorithms.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, 8837:98–114. Society of Industrial and Applied Mathematics, 2014. https://doi.org/10.1007/978-3-319-11936-6_8. ieee: T. Brázdil et al., “Verification of markov decision processes using learning algorithms,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Sydney, Australia, 2014, vol. 8837, pp. 98–114. ista: 'Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretinsky J, Kwiatkowska M, Parker D, Ujma M. 2014. Verification of markov decision processes using learning algorithms. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ALENEX: Algorithm Engineering and Experiments, LNCS, vol. 8837, 98–114.' mla: Brázdil, Tomáš, et al. “Verification of Markov Decision Processes Using Learning Algorithms.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, vol. 8837, Society of Industrial and Applied Mathematics, 2014, pp. 98–114, doi:10.1007/978-3-319-11936-6_8. short: T. Brázdil, K. Chatterjee, M. Chmelik, V. Forejt, J. Kretinsky, M. Kwiatkowska, D. Parker, M. Ujma, in:, F. Cassez, J.-F. Raskin (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Society of Industrial and Applied Mathematics, 2014, pp. 98–114. conference: end_date: 2014-11-07 location: Sydney, Australia name: 'ALENEX: Algorithm Engineering and Experiments' start_date: 2014-11-03 date_created: 2018-12-11T11:55:17Z date_published: 2014-11-01T00:00:00Z date_updated: 2021-01-12T06:54:49Z day: '01' department: - _id: KrCh - _id: ToHe doi: 10.1007/978-3-319-11936-6_8 ec_funded: 1 editor: - first_name: Franck full_name: Cassez, Franck last_name: Cassez - first_name: Jean-François full_name: Raskin, Jean-François last_name: Raskin intvolume: ' 8837' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1402.2967 month: '11' oa: 1 oa_version: Submitted Version page: 98 - 114 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 26241A12-B435-11E9-9278-68D0E5697425 grant_number: '24696' name: LIGHT-REGULATED LIGAND TRAPS FOR SPATIO-TEMPORAL INHIBITION OF CELL SIGNALING - _id: 2581B60A-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '279307' name: 'Quantitative Graph Games: Theory and Applications' - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms - _id: 25863FF4-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11407 name: Game Theory - _id: 2584A770-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: P 23499-N23 name: Modern Graph Algorithmic Techniques in Formal Verification - _id: 2587B514-B435-11E9-9278-68D0E5697425 name: Microsoft Research Faculty Fellowship publication: ' Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)' publication_status: published publisher: Society of Industrial and Applied Mathematics publist_id: '5046' quality_controlled: '1' status: public title: Verification of markov decision processes using learning algorithms type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 8837 year: '2014' ... --- _id: '2026' abstract: - lang: eng text: 'We present a tool for translating LTL formulae into deterministic ω-automata. It is the first tool that covers the whole LTL that does not use Safra’s determinization or any of its variants. This leads to smaller automata. There are several outputs of the tool: firstly, deterministic Rabin automata, which are the standard input for probabilistic model checking, e.g. for the probabilistic model-checker PRISM; secondly, deterministic generalized Rabin automata, which can also be used for probabilistic model checking and are sometimes by orders of magnitude smaller. We also link our tool to PRISM and show that this leads to a significant speed-up of probabilistic LTL model checking, especially with the generalized Rabin automata.' acknowledgement: "Sponsor: P202/12/G061; GACR; Czech Science Foundation\r\n\r\n" alternative_title: - LNCS author: - first_name: Zuzana full_name: Komárková, Zuzana last_name: Komárková - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: ama: 'Komárková Z, Kretinsky J. Rabinizer 3: Safraless translation of ltl to small deterministic automata. In: Cassez F, Raskin J-F, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8837. Springer; 2014:235-241. doi:10.1007/978-3-319-11936-6_17' apa: 'Komárková, Z., & Kretinsky, J. (2014). Rabinizer 3: Safraless translation of ltl to small deterministic automata. In F. Cassez & J.-F. Raskin (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8837, pp. 235–241). Sydney, Australia: Springer. https://doi.org/10.1007/978-3-319-11936-6_17' chicago: 'Komárková, Zuzana, and Jan Kretinsky. “Rabinizer 3: Safraless Translation of Ltl to Small Deterministic Automata.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, 8837:235–41. Springer, 2014. https://doi.org/10.1007/978-3-319-11936-6_17.' ieee: 'Z. Komárková and J. Kretinsky, “Rabinizer 3: Safraless translation of ltl to small deterministic automata,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Sydney, Australia, 2014, vol. 8837, pp. 235–241.' ista: 'Komárková Z, Kretinsky J. 2014. Rabinizer 3: Safraless translation of ltl to small deterministic automata. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 8837, 235–241.' mla: 'Komárková, Zuzana, and Jan Kretinsky. “Rabinizer 3: Safraless Translation of Ltl to Small Deterministic Automata.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, vol. 8837, Springer, 2014, pp. 235–41, doi:10.1007/978-3-319-11936-6_17.' short: Z. Komárková, J. Kretinsky, in:, F. Cassez, J.-F. Raskin (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer, 2014, pp. 235–241. conference: end_date: 2014-11-07 location: Sydney, Australia name: 'ATVA: Automated Technology for Verification and Analysis' start_date: 2014-11-03 date_created: 2018-12-11T11:55:17Z date_published: 2014-01-01T00:00:00Z date_updated: 2021-01-12T06:54:49Z day: '01' department: - _id: ToHe doi: 10.1007/978-3-319-11936-6_17 ec_funded: 1 editor: - first_name: Franck full_name: Cassez, Franck last_name: Cassez - first_name: Jean-François full_name: Raskin, Jean-François last_name: Raskin intvolume: ' 8837' language: - iso: eng month: '01' oa_version: None page: 235 - 241 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms publication: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) publication_status: published publisher: Springer publist_id: '5045' quality_controlled: '1' status: public title: 'Rabinizer 3: Safraless translation of ltl to small deterministic automata' type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 8837 year: '2014' ... --- _id: '2053' abstract: - lang: eng text: In contrast to the usual understanding of probabilistic systems as stochastic processes, recently these systems have also been regarded as transformers of probabilities. In this paper, we give a natural definition of strong bisimulation for probabilistic systems corresponding to this view that treats probability distributions as first-class citizens. Our definition applies in the same way to discrete systems as well as to systems with uncountable state and action spaces. Several examples demonstrate that our definition refines the understanding of behavioural equivalences of probabilistic systems. In particular, it solves a longstanding open problem concerning the representation of memoryless continuous time by memoryfull continuous time. Finally, we give algorithms for computing this bisimulation not only for finite but also for classes of uncountably infinite systems. acknowledgement: This work is supported by the EU 7th Framework Programme under grant agreements 295261 (MEALS) and 318490 (SENSATION), Czech Science Foundation under grant agreement P202/12/G061, the DFG Transregional Collaborative Research Centre SFB/TR 14 AVACS, and by the CAS/SAFEA International Partnership Program for Creative Research Teams. alternative_title: - LNCS author: - first_name: Holger full_name: Hermanns, Holger last_name: Hermanns - first_name: Jan full_name: Krčál, Jan last_name: Krčál - first_name: Jan full_name: Kretinsky, Jan id: 44CEF464-F248-11E8-B48F-1D18A9856A87 last_name: Kretinsky orcid: 0000-0002-8122-2881 citation: ama: 'Hermanns H, Krčál J, Kretinsky J. Probabilistic bisimulation: Naturally on distributions. In: Baldan P, Gorla D, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:249-265. doi:10.1007/978-3-662-44584-6_18' apa: 'Hermanns, H., Krčál, J., & Kretinsky, J. (2014). Probabilistic bisimulation: Naturally on distributions. In P. Baldan & D. Gorla (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704, pp. 249–265). Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-662-44584-6_18' chicago: 'Hermanns, Holger, Jan Krčál, and Jan Kretinsky. “Probabilistic Bisimulation: Naturally on Distributions.” In Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, 8704:249–65. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. https://doi.org/10.1007/978-3-662-44584-6_18.' ieee: 'H. Hermanns, J. Krčál, and J. Kretinsky, “Probabilistic bisimulation: Naturally on distributions,” in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Rome, Italy, 2014, vol. 8704, pp. 249–265.' ista: 'Hermanns H, Krčál J, Kretinsky J. 2014. Probabilistic bisimulation: Naturally on distributions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). CONCUR: Concurrency Theory, LNCS, vol. 8704, 249–265.' mla: 'Hermanns, Holger, et al. “Probabilistic Bisimulation: Naturally on Distributions.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–65, doi:10.1007/978-3-662-44584-6_18.' short: H. Hermanns, J. Krčál, J. Kretinsky, in:, P. Baldan, D. Gorla (Eds.), Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–265. conference: end_date: 2014-09-05 location: Rome, Italy name: 'CONCUR: Concurrency Theory' start_date: 2014-09-02 date_created: 2018-12-11T11:55:27Z date_published: 2014-09-01T00:00:00Z date_updated: 2021-01-12T06:55:00Z day: '01' department: - _id: ToHe - _id: KrCh doi: 10.1007/978-3-662-44584-6_18 ec_funded: 1 editor: - first_name: Paolo full_name: Baldan, Paolo last_name: Baldan - first_name: Daniele full_name: Gorla, Daniele last_name: Gorla intvolume: ' 8704' language: - iso: eng main_file_link: - open_access: '1' url: http://arxiv.org/abs/1404.5084 month: '09' oa: 1 oa_version: Submitted Version page: 249 - 265 project: - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling - _id: 25F5A88A-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S11402-N23 name: Moderne Concurrency Paradigms publication: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '4993' status: public title: 'Probabilistic bisimulation: Naturally on distributions' type: conference user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87 volume: 8704 year: '2014' ...