Publications

Journals

2017

Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games

Mária SVOREŇOVÁ, Jan KŘETÍNSKÝ, Martin CHMELÍK, Krishnendu CHATTERJEE, Ivana ČERNÁ and Calin BELTA.
Nonlinear Analysis: Hybrid Systems, Elsevier, 2017, Vol. 23, February 2017, pp. 230-253. ISSN 1751-570X.

More details

Trading performance for stability in Markov decision processes

Tomáš BRÁZDIL, Krishnendu CHATTERJEE, Vojtěch FOREJT and Antonín KUČERA.
Journal of Computer and System Sciences, SAN DIEGO: Elsevier, 2017, Vol. 84, No. 2017, pp. 144-170. ISSN 0022-0000.

More details

First order limits of sparse graphs: Plane trees and path-width

Jakub GAJARSKÝ, Petr HLINĚNÝ, Tomáš KAISER, Daniel KRÁĽ, Martin KUPEC, Jan OBDRŽÁLEK, Sebastian ORDYNIAK and Vojtěch TŮMA.
Random Structures & Algorithms, Wiley, 2017. ISSN 1098-2418.

More details

Kernelization using structural parameters on sparse graph classes

Jakub GAJARSKÝ, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Sebastian ORDYNIAK, Felix REIDL, Peter ROSSMANITH, Fernando VILLAAMIL and Somnath SIKDAR.
Journal of Computer and System Sciences, SAN DIEGO: Elsevier, 2017, Vol. 84, No. 1, pp. 219-242. ISSN 0022-0000.

More details

Parameterized Extension Complexity of Independent Set and Related Problems

Jakub GAJARSKÝ, Petr HLINĚNÝ and Hans Raj TIWARY.
Discrete Applied Mathematics, Elsevier Science, 2017. ISSN 0166-218X.

More details

A tighter insertion-based approximation of the crossing number

Markus CHIMANI and Petr HLINĚNÝ.
Journal of Combinatorial Optimization, Springer, 2017. ISSN 1573-2886.

More details

2016

From LTL to deterministic automata (A safraless compositional approach)

Javier ESPARZA, Jan KŘETÍNSKÝ and Salomon SICKERT.
Formal Methods in System Design, Springer Netherlands, 2016, Vol. 49, No. 3, pp. 219-271. ISSN 0925-9856.

More details

Are there any good digraph width measures?

Robert GANIAN, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Joachim KNEIS, Daniel MEISTER, Somnath SIKDAR and Peter ROSSMANITH.
Journal of Combinatorial Theory, Ser B, Academic Press, 2016, Vol. 116, No. 1, pp. 250-286. ISSN 0095-8956.

More details

Tree-depth and Vertex-minors

Petr HLINĚNÝ, O-joung KWON, Jan OBDRŽÁLEK and Sebastian ORDYNIAK.
European Journal of Combinatorics, Elsevier, 2016, Vol. 56, No. 1, pp. 46-56. ISSN 0195-6698.

More details

2015

Refinement checking on parametric modal transition systems

Nikola BENEŠ, Jan KŘETÍNSKÝ, Kim G. LARSEN, Mikael H. MOLLER, Salomon SICKERT and Jiří SRBA.
Acta Informatica, Springer, 2015, Vol. 52, 2-3, pp. 269-297. ISSN 0001-5903.

More details

Runtime analysis of probabilistic programs with unbounded recursion

Tomáš BRÁZDIL, Stefan KIEFER, Antonín KUČERA and Ivana HUTAŘOVÁ VAŘEKOVÁ.
Journal of Computer and System Sciences, Academic Press, 2015, Vol. 81, No. 1, pp. 288-310. ISSN 0022-0000.

More details

Planar Emulators Conjecture Is Nearly True for Cubic Graphs

Martin DERKA and Petr HLINĚNÝ.
European Journal of Combinatorics, Elsevier, 2015, Vol. 48, No. 1, pp. 63-70. ISSN 0195-6698.

More details

Faster Existential FO Model Checking on Posets

Jakub GAJARSKÝ, Petr HLINĚNÝ, Jan OBDRŽÁLEK and Sebastian ORDYNIAK.
Logical Methods in Computer Science, Německo: Logical Methods in Computer Science e.V., 2015, Vol. 11, No. 4, pp. 1-13. ISSN 1860-5974.

More details

Kernelizing MSO Properties of Trees of Fixed Height, and Some Consequences

Jakub GAJARSKÝ and Petr HLINĚNÝ.
Logical Methods in Computer Science, Německo: Logical Methods in Computer Science e.V., 2015, Vol. 11, No. 1, pp. 1-26. ISSN 1860-5974.

More details

FO Model Checking of Interval Graphs

Robert GANIAN, Petr HLINĚNÝ, Daniel KRÁĽ, Jan OBDRŽÁLEK, Jarett SCHWARTZ and Jakub TESKA.
Logical Methods in Computer Science, Německo: Logical Methods in Computer Science e.V., 2015, Vol. 11, 4:11, pp. 1-20. ISSN 1860-5974.

More details

2014

Branching-time model-checking of probabilistic pushdown automata

Tomáš BRÁZDIL, Václav BROŽEK, Vojtěch FOREJT and Antonín KUČERA.
Journal of Computer and System Sciences, Academic Press, 2014, Vol. 80, No. 1, pp. 139-156. ISSN 0022-0000.

More details

Efficient Analysis of Probabilistic Programs with an Unbounded Counter

Tomáš BRÁZDIL, Stefan KIEFER and Antonín KUČERA.
Journal of the ACM, New York, NY, USA: ACM, 2014, Vol. 61, No. 6, pp. 1-35. ISSN 0004-5411.

More details

Markov Decision Processes with Multiple Long-Run Average Objectives

Tomáš BRÁZDIL, Václav BROŽEK, Krishnendu CHATTERJEE, Vojtěch FOREJT and Antonín KUČERA.
Logical Methods in Computer Science, Technical University of Braunschweig, 2014, Vol. 10, No. 1, pp. 1-29. ISSN 1860-5974.

More details

Computing the stretch of an embedded graph

Sergio CABELLO, Markus CHIMANI and Petr HLINĚNÝ.
SIAM Journal on Discrete Mathematics, Philadelphia: SIAM, 2014, Vol. 28, No. 3, pp. 1391-1401. ISSN 0895-4801.

More details

Digraph width measures in parameterized algorithmics

Robert GANIAN, Petr HLINĚNÝ, Joachim KNEIS, Alexander LANGER, Jan OBDRŽÁLEK and Peter ROSSMANITH.
Discrete Applied Mathematics, Elsevier B.V., 2014, Vol. 168, No. 1, pp. 88-107. ISSN 0166-218X.

More details

Lower Bounds on the Complexity of MSO_1 Model-Checking

Robert GANIAN, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Alexander LANGER, Peter ROSSMANITH and Somnath SIKDAR.
Journal of Computer and System Sciences, Elsevier, 2014, Vol. 80, No. 1, pp. 180-194. ISSN 0022-0000.

More details

2013

Analyzing probabilistic pushdown automata

Tomáš BRÁZDIL, Javier ESPARZA, Stefan KIEFER and Antonín KUČERA.
Formal Methods in System Design, Springer Netherlands, 2013, Vol. 43, No. 2, pp. 124-163. ISSN 0925-9856.
Preprint.

More details

Approximating the termination value of one-counter MDPs and stochastic games

Tomáš BRÁZDIL, Václav BROŽEK, Kousha ETESSAMI and Antonín KUČERA.
Information and Computation, Netherlands: Elsevier Science, 2013, Vol. 222, January, pp. 121-138. ISSN 0890-5401.
Preprint.

More details

Continuous-Time Stochastic Games with Time-Bounded Reachability

Tomáš BRÁZDIL, Vojtěch FOREJT, Jan KRČÁL, Jan KŘETÍNSKÝ and Antonín KUČERA.
Information and Computation, Elsevier, 2013, Vol. 224, No. 1, pp. 46-70. ISSN 0890-5401.

More details

How Not to Characterize Planar-emulable Graphs

Petr HLINĚNÝ, Martin DERKA, Markus CHIMANI and Matěj KLUSÁČEK.
Advances in Applied Mathematics, Holandsko: Elsevier, 2013, Vol. 50, No. 1, pp. 46-68. ISSN 0196-8858.

More details

Better algorithms for satisfiability problems for formulas of bounded rank-width

Robert GANIAN, Petr HLINĚNÝ and Jan OBDRŽÁLEK.
Fundamenta Informaticae, Poland: IOS Press, The Netherlands, 2013, Vol. 123, No. 1, pp. 59-76. ISSN 0169-2968.

More details

Unified Approach to Polynomial Algorithms on Graphs of Bounded (bi-)Rank-width

Robert GANIAN, Petr HLINĚNÝ and Jan OBDRŽÁLEK.
European Journal of Combinatorics, Elsevier, 2013, Vol. 34, No. 3, pp. 680-701. ISSN 0195-6698.

More details

2012

Stochastic game logic

Christel BAIER, Tomáš BRÁZDIL, Marcus GRÖSSER and Antonín KUČERA.
Acta informatica, Berlin: Springer-Verlag, 2012, Vol. 49, No. 4, pp. 203-224. ISSN 0001-5903.

More details

The DAG-width of directed graphs

Dietmar BERWANGER, Anuj DAWAR, Paul HUNTER, Stephan KREUTZER and Jan OBDRŽÁLEK.
Journal of Combinatorial Theory, Ser B, Amsterdam: Elsevier B.V., 2012, Vol. 102, No. 4, pp. 900-923. ISSN 0095-8956.

More details

Space-efficient scheduling of stochastically generated tasks

Tomáš BRÁZDIL, Javier ESPARZA, Stefan KIEFER and Michael LUTTENBERGER.
Information and Computation, Elsevier, 2012, Vol. 210, January, pp. 87–110. ISSN 0890-5401.

More details

Generalized Maneuvers in Route Planning

Petr HLINĚNÝ and Ondrej MORIŠ.
Computing and Informatics, Bratislava: Slovak Academy of Sciences, 2012, Vol. 31, No. 3, pp. 531-549. ISSN 1335-9150.

More details

Vertex insertion approximates the crossing number of apex graphs

Petr HLINĚNÝ, Markus CHIMANI and Petra MUTZEL.
European Journal of Combinatorics, Elsevier, 2012, Vol. 33, No. 3, pp. 326-335. ISSN 0195-6698.

More details

Conference Proceedings

2017

Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms

Christel BAIER, Clemens DUBSLAFF, Ľuboš KORENČIAK, Antonín KUČERA and Vojtěch ŘEHÁK.
In Nathalie Bertrand, Luca Bortolussi. Quantitative Evaluation of Systems. Pages 190-206.

More details

Synthesis of Optimal Resilient Control Strategies

Christel BAIER, Clemens DUBSLAFF, Ľuboš KORENČIAK, Antonín KUČERA and Vojtěch ŘEHÁK.
In Deepak D'Souza, K. Narayan Kumar. Automated Technology for Verification and Analysis. Pages 417-434.

More details

On Colourability of Polygon Visibility Graphs

Onur CAGIRICI, Petr HLINĚNÝ and Bodhayan ROY.
In FSTTCS 2017..

More details

Parameterized Shifted Combinatorial Optimization

Jakub GAJARSKÝ, Petr HLINĚNÝ, Martin KOUTECKÝ and Shmuel ONN.
In Y. Cao and J. Chen. International Computing and Combinatorics Conference COCOON 2017 (LNCS, volume 10392). Pages 224-236.

More details

FO model checking of geometric graphs

Petr HLINĚNÝ, Filip POKRÝVKA and Bodhayan ROY.
In IPEC 2017..

More details

Symbiotic 4: Beyond Reachability (Competition Contribution)

Marek CHALUPA, Martina VITOVSKÁ, Martin JONÁŠ, Jiří SLABÝ and Jan STREJČEK.
In Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference. Pages 385-389.

More details

On Simplification of Formulas with Unconstrained Variables and Quantifiers

Martin JONÁŠ and Jan STREJČEK.
In Serge Gaspers, Toby Walsh. Theory and Applications of Satisfiability Testing – SAT 2017. Pages 364-379.

More details

2016

Policy Learning for Time-Bounded Reachability in Continuous-Time Markov Decision Processes via Doubly-Stochastic Gradient Ascent

Tomáš BRÁZDIL, Ezio BARTOCCI, Dimitrios MILIOS, Guido SANGUINETTI and Luca BORTOLUSSI.
In Proceedings of QEST 2016. Pages 244-259.

More details

Complementing Semi-deterministic Büchi Automata

František BLAHOUDEK, Matthias HEIZMANN, Sven SCHEWE, Jan STREJČEK and Ming-Hsien TSAI.
In Marsha Chechik, Jean-François Raskin. Tools and Algorithms for the Construction and Analysis of Systems 22nd International Conference, TACAS 2016. Pages 770-787.

More details

Optimizing the Expected Mean Payoff in Energy Markov Decision Processes

Tomáš BRÁZDIL, Antonín KUČERA and Petr NOVOTNÝ.
In Cyrille Artho, Axel Legay, Doron Peled. Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016. Pages 32-49.

More details

Stability in Graphs and Games

Tomáš BRÁZDIL, Vojtěch FOREJT, Antonín KUČERA and Petr NOVOTNÝ.
In Josee Desharnais, Radha Jagadeesan. 27th International Conference on Concurrency Theory, CONCUR 2016. Pages 1-14.

More details

Stochastic Shortest Path with Energy Constraints in POMDPs: (Extended Abstract)

Tomáš BRÁZDIL, Petr NOVOTNÝ, Krishnendu CHATTERJEE, Martin CHMELÍK and Anchit GUPTA.
In Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems. Pages 1465-1466.

More details

Tighter Loop Bound Analysis

Pavel ČADEK, Jan STREJČEK and Marek TRTÍK.
In Cyrille Artho and Axel Legay and Doron Peled. Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016. Pages 512-527.

More details

Faster Statistical Model Checking for Unbounded Temporal Properties

Przemyslaw DACA, Thomas A. HENZINGER, Jan KŘETÍNSKÝ and Tatjana PETROV.
In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016. Pages 112-129.

More details

Linear Distances between Markov Chains

Przemyslaw DACA, Thomas A. HENZINGER, Jan KŘETÍNSKÝ and Tatjana PETROV.
In 27th International Conference on Concurrency Theory, CONCUR 2016. Pages 1-15.

More details

Crossing Number is Hard for Kernelization

Marek DERŇÁR and Petr HLINĚNÝ.
In 32nd International Symposium on Computational Geometry (SoCG 2016). Pages "42:1"-"42:10".

More details

Limit-Deterministic Büchi Automata for Linear Temporal Logic

Salomon SICKERT, Javier ESPARZA, Stefan JAAX and Jan KŘETÍNSKÝ.
In Computer Aided Verification - 28th International Conference, CAV 2016. Pages 312-332.

More details

Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC

Ľuboš KORENČIAK, Vojtěch ŘEHÁK and Adrian FARMADIN.
In Erika Ábrahám, Marieke Huisman. Integrated Formal Methods. Pages 130-138.

More details

A New Perspective on FO Model Checking of Dense Graph Classes

Jakub GAJARSKÝ, Petr HLINĚNÝ, Daniel LOKSHTANOV, Jan OBDRŽÁLEK and M S RAMANUJAN.
In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science LICS2016. Pages 176-184.

More details

Inserting Multiple Edges into a Planar Graph

Markus CHIMANI and Petr HLINĚNÝ.
In 32nd International Symposium on Computational Geometry (SoCG 2016). Pages "30:1"-"30:15".

More details

Practical Exhaustive Generation of Small Multiway Cuts in Sparse Graphs

Petr HLINĚNÝ and Ondřej SLÁMEČKA.
In Jan Kofroň, Tomáš Vojnar. Mathematical and Engineering Methods in Computer Science, Lecture Notes in Computer Science 9548. Pages 54-66.

More details

Symbiotic 3: New Slicer and Error-Witness Generation (Competition Contribution)

Marek CHALUPA, Martin JONÁŠ, Jiří SLABÝ, Jan STREJČEK and Martina VITOVSKÁ.
In Marsha Chechik and Jean-Francois Raskin. Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016. Pages 946-949.

More details

Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams

Martin JONÁŠ and Jan STREJČEK.
In Nadia Creignou and Daniel Le Berre. Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference. Pages 267-283.

More details

Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration

Ľuboš KORENČIAK, Antonín KUČERA and Vojtěch ŘEHÁK.
In 2016 IEEE 24th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. Pages 367-372.

More details

MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata

Salomon SICKERT and Jan KŘETÍNSKÝ.
In Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016. Pages 130-137.

More details

Survey of Statistical Verification of Linear Unbounded Properties: Model Checking and Distances

Jan KŘETÍNSKÝ.
In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016. Pages 27-45.

More details

2015

The Hanoi Omega-Automata Format

Tomáš BABIAK, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, Jan KŘETÍNSKÝ, David MÜLLER, David PARKER and Jan STREJČEK.
In Daniel Kroening, Corina Pasareanu. Computer Aided Verification: 27th International Conference, CAV 2015. Pages 479-486.

More details

Temporal Logic Control for Stochastic Linear Systems using Abstraction Refinement of Probabilistic Games

Mária SVOREŇOVÁ, Jan KŘETÍNSKÝ, Martin CHMELÍK, Krishnendu CHATTERJEE, Ivana ČERNÁ and Calin BELTA.
In Proceedings of ACM international conference on Hybrid Systems: Computation and Control. Pages 259-268.

More details

Complete Composition Operators for IOCO-Testing Theory

Nikola BENEŠ, Przemysław DACA, Thomas A. HENZINGER, Jan KŘETÍNSKÝ and Dejan NIČKOVIĆ.
In Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering. Pages 101-110.

More details

On Refinement of Büchi Automata for Explicit Model Checking

František BLAHOUDEK, Alexandre DURET-LUTZ, Vojtěch RUJBR and Jan STREJČEK.
In Fischer, Bernd and Geldenhuys, Jaco. 2015 International SPIN Symposium on Model Checking of Software. Pages 66-83.

More details

On Degree Properties of Crossing-critical Families of Graphs

Drago BOKAL, Mojca BRAČIČ, Marek DERŇÁR and Petr HLINĚNÝ.
In Emilio Di Giacomo, Anna Lubiw. Graph Drawing and Network Visualization 2015, Lecture Notes in Computer Science 9411. Pages 75-86.

More details

Counterexample Explanation by Learning Small Strategies in Markov Decision Processes

Tomáš BRÁZDIL, Krishnendu CHATTERJEE, Martin CHMELÍK, Andreas FELLNER and Jan KŘETÍNSKÝ.
In Daniel Kroening, Corina Pasareanu. Computer Aided Verification: 27th International Conference, CAV 2015. Pages 158-177.

More details

Long-Run Average Behaviour of Probabilistic Vector Addition Systems

Tomáš BRÁZDIL, Stefan KIEFER, Antonín KUČERA and Petr NOVOTNÝ.
In Neuveden. 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015. Pages 44-55.

More details

MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives

Tomáš BRÁZDIL, Chatterjee KRISHNENDU, Vojtěch FOREJT and Antonín KUČERA.
In Christel Baier, Cesare Tinelli. Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Pages 181-187.

More details

Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis

Tomáš BRÁZDIL, Ľuboš KORENČIAK, Jan KRČÁL, Petr NOVOTNÝ and Vojtěch ŘEHÁK.
In Javier Campos, Boudewijn R. Haverkort. Quantitative Evaluation of Systems. Pages 141-159.

More details

Optimal Continuous Time Markov Decisions

Yuliya BUTKOVA, Hassan HATEFI, Holger HERMANNS and Jan KRČÁL.
In ATVA 2015. Pages 166-182.

More details

Compositionality for Quantitative Specifications

Uli FAHRENBERG, Jan KŘETÍNSKÝ, Axel LEGAY and Louis-Marie TRAONOUEZ.
In The 11th International Symposium on Formal Aspects of Component Software - FACS 2014. Pages 306-324.

More details

Controller Synthesis for MDPs and Frequency LTL\GU

Vojtěch FOREJT, Jan KRČÁL and Jan KŘETÍNSKÝ.
In LPAR 2015. Pages 162-177.

More details

On Frequency LTL in Probabilistic Systems

Vojtěch FOREJT and Jan KRČÁL.
In CONCUR 2015. Pages 184-197.

More details

FO Model Checking on Posets of Bounded Width

Jakub GAJARSKÝ, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Sebastian ORDYNIAK, M.S. RAMANUJAN, Daniel LOKSHTANOV and Saket SAURABH.
In Venkatesan Guruswami. 56th Annual Symposium on Foundations of Computer Science, FOCS 2015. Pages 963 - 974.

More details

On Hardness of the Joint Crossing Number

Petr HLINĚNÝ and Gelasio SALAZAR.
In Khaled Elbassioni, Kazuhisa Makino. International Symposium on Algorithms and Computation (ISAAC 2015), Lecture Notes in Computer Science 9472. Pages 603-613.

More details

Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes

Krishnendu CHATTERJEE, Zuzana KOMÁRKOVÁ and Jan KŘETÍNSKÝ.
In Thirtieth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Pages 244-256.

More details

Scalable Analysis of Fault Trees with Dynamic Features

Jan KRČÁL and Pavel KRČÁL.
In DSN 2015. Pages 89-100.

More details

Polynomial Time Decidability of Weighted Synchronization under Partial Observability

Jan KŘETÍNSKÝ, Kim Guldstrand LARSEN, Simon LAURSEN and Jiří SRBA.
In 26th International Conference on Concurrency Theory (CONCUR 2015). Pages 142-154.

More details

2014

Solving adversarial patrolling games with bounded error: (extended abstract)

Michal ABAFFY, Tomáš BRÁZDIL, Vojtěch ŘEHÁK, Branislav BOŠANSKÝ, Antonín KUČERA and Jan KRČÁL.
In Alessio Lomuscio, Paul Scerri, Ana Bazzan, and Michael Huhns. Proceedings of the 13th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'14). Pages 1617-1618.

More details

Is there a best Büchi automaton for explicit model checking?

František BLAHOUDEK, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ and Jan STREJČEK.
In Neha Rungta and Oksana Tkachuk. 2014 International SPIN Symposium on Model Checking of Software. Pages 68-143.
Preprint.

More details

Minimizing Running Costs in Consumption Systems

Tomáš BRÁZDIL, David KLAŠKA, Antonín KUČERA and Petr NOVOTNÝ.
In Armin Biere, Roderick Bloem. Computer Aided Verification. Pages 457-472.

More details

Verification of Markov Decision Processes using Learning Algorithms

Tomáš BRÁZDIL, Krishnendu CHATTERJEE, Martin CHMELÍK, Vojtěch FOREJT, Jan KŘETÍNSKÝ, Marta KWIATKOWSKA, David PARKER and Mateusz UJMA.
In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014. Pages 98-114.

More details

Zero-reachability in probabilistic multi-counter automata

Tomáš BRÁZDIL, Stefan KIEFER, Antonín KUČERA, Petr NOVOTNÝ and Joost-Pieter KATOEN.
In Thomas Henzinger and Dale Miller. Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Pages nestránkováno.

More details

Faster Existential FO Model Checking on Posets

Jakub GAJARSKÝ, Petr HLINĚNÝ, Jan OBDRŽÁLEK and Sebastian ORDYNIAK.
In Hee-Kap Ahn, Chan-Su Shin. ISAAC 2014, LNCS 8889. Pages 441-451.

More details

Dealing with Zero Density Using Piecewise Phase-Type Approximation

Ľuboš KORENČIAK, Jan KRČÁL and Vojtěch ŘEHÁK.
In András Horváth, Katinka Wolter. Computer Performance Engineering. Pages 119-134.

More details

Symbiotic 2: More Precise Slicing (Competition Contribution)

Jiří SLABÝ and Jan STREJČEK.
In E. Ábrahám and K. Havelund. Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014. Pages 415-417.

More details

Symbolic Memory with Pointers

Marek TRTÍK and Jan STREJČEK.
In Franck Cassez and Jean-Francois Raskin. Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014. Pages 380-395.

More details

2013

Compositional Approach to Suspension and Other Improvements to LTL Translation

Tomáš BABIAK, Thomas BADIE, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ and Jan STREJČEK.
In Ezio Bartocci, C. R. Ramakrishnan. Model Checking Software - 20th International Symposium, SPIN 2013. Pages 81-98.

More details

Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment

František BLAHOUDEK, Tomáš BABIAK, Mojmír KŘETÍNSKÝ and Jan STREJČEK.
In Hung Dang-Van and Mizuhito Ogawa. 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013. Pages 24-38.

More details

Comparison of LTL to Deterministic Rabin Automata Translators

František BLAHOUDEK, Mojmír KŘETÍNSKÝ and Jan STREJČEK.
In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov. Logic for Programming Artificial Intelligence and Reasoning, LPAR-19. Pages 164-172.

More details

Determinacy in Stochastic Games with Unbounded Payoff Functions

Tomáš BRÁZDIL, Antonín KUČERA and Petr NOVOTNÝ.
In Mathematical and Engineering Methods in Computer Science (MEMICS 2012). Pages 94-105.

More details

On time-average limits in deterministic and stochastic Petri nets

Tomáš BRÁZDIL, Ľuboš KORENČIAK, Jan KRČÁL, Jan KŘETÍNSKÝ and Vojtěch ŘEHÁK.
In ACM/SPEC International Conference on Performance Engineering, ICPE'13. Pages 421-422.

More details

Solvency Markov Decision Processes with Interest

Tomáš BRÁZDIL, Taolue CHEN, Vojtěch FOREJT, Petr NOVOTNÝ and Aistis SIMAITIS.
In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Pages 487-499.

More details

Trading Performance for Stability in Markov Decision Processes

Tomáš BRÁZDIL, Krishnendu CHATTERJEE, Vojtěch FOREJT and Antonín KUČERA.
In Proceedings of 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013). Pages 331-340.

More details

Planar Emulators Conjecture Is Nearly True for Cubic Graphs

Petr HLINĚNÝ and Martin DERKA.
In J. Nešetřil, M. Pellegrini. The Seventh European Conference on Combinatorics, Graph Theory and Applications - Eurocomb 2013. Pages 245-250.

More details

Kernelization Using Structural Parameters on Sparse Graph Classes

Jakub GAJARSKÝ, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Sebastian ORDYNIAK, Felix REIDL, Peter ROSSMANITH, Fernando Sanchez VILLAAMIL and Somnath SIKDAR.
In Hans L. Bodlaender a Giuseppe F. Italiano. ESA 2013. Pages 529-540.

More details

Expanding the Expressive Power of Monadic Second-Order Logic on Restricted Graph Classes

Jan OBDRŽÁLEK and Robert GANIAN.
In Thierry Lecroq, Laurent Mouchard. Combinatorial Algorithms 24th International Workshop, IWOCA 2013. Pages 164-177.

More details

FO Model Checking of Interval Graphs

Robert GANIAN, Petr HLINĚNÝ, Daniel KRÁĽ, Jan OBDRŽÁLEK, Jarett SCHWARTZ and Jakub TESKA.
In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, David Peleg. ICALP (2) 2013. Pages 250-262.

More details

Compositional Verification and Optimization of Interactive Markov Chains

Holger HERMANNS, Jan KRČÁL and Jan KŘETÍNSKÝ.
In CONCUR 2013 - Concurrency Theory - 24th International Conference. Pages 364-379.

More details

Controllable-choice Message Sequence Graphs

Martin CHMELÍK and Vojtěch ŘEHÁK.
In Proceedings of Mathematical and Engineering Methods in Computer Science, 8th Doctoral Workshop (MEMICS 2012), Selected Papers. Pages 118-130.

More details

ClabureDB: Classified Bug-Reports Database Tool for Developers of Program Analysis Tools

Jiří SLABÝ, Jan STREJČEK and Marek TRTÍK.
In Roberto Giacobazzi, Josh Berdine, Isabella Mastroeni. Verification, Model Checking, and Abstract Interpretation: 14th International Conference, VMCAI 2013. Pages 268-274.
Preprint.

More details

Compact Symbolic Execution

Jiří SLABÝ, Jan STREJČEK and Marek TRTÍK.
In Hung Dang-Van and Mizuhito Ogawa. 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013. Pages 193-207.

More details

Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution)

Jiří SLABÝ, Jan STREJČEK and Marek TRTÍK.
In Nir Piterman, Scott A. Smolka. Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013. Pages 630-632.
Preprint.

More details

2012

Efficient Controller Synthesis for Consumption Games with Multiple Resource Types

Tomáš BRÁZDIL, Krishnendu CHATTERJEE, Antonín KUČERA and Petr NOVOTNÝ.
In Computer Aided Verification - 24th International Conference, CAV 2012. Pages 23-38.

More details

Minimizing Expected Termination Time in One-Counter Markov Decision Processes

Tomáš BRÁZDIL, Antonín KUČERA, Petr NOVOTNÝ and Dominik WOJTCZAK.
In Proceedings of 39th International Colloquium on Automata, Languages and Programming (ICALP 2012). Pages 141-152.

More details

Stabilization of Branching Queueing Networks

Tomáš BRÁZDIL and Stefan KIEFER.
In Proceedings of the 29th International Symposium on Theoretical Aspects of Computer Science. Pages 507-518.

More details

Verification of Open Interactive Markov Chains

Tomáš BRÁZDIL, Holger HERMANNS, Jan KRČÁL, Jan KŘETÍNSKÝ and Vojtěch ŘEHÁK.
In Deepak D'Souza and Telikepalli Kavitha and Jaikumar Radhakrishnan. IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Pages 474-485.

More details

Faster Deciding MSO Properties of Trees of Fixed Height, and Some Consequences

Jakub GAJARSKÝ and Petr HLINĚNÝ.
In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Pages 112-123.

More details

Lower Bounds on the Complexity of MSO_1 Model-Checking

Robert GANIAN, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Alexander LANGER, Peter ROSSMANITH and Somnath SIKDAR.
In 29th International Symposium on Theoretical Aspects of Computer Science STACS2012. Pages 326-337.

More details

When Trees Grow Low: Shrubs and Fast MSO1

Robert GANIAN, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Jaroslav NEŠETŘIL, Patrice OSSONA DE MENDEZ and Reshma RAMADURAI.
In Math Foundations of Computer Science MFCS 2012. Pages 419-430.

More details

Other Publications

2012

Sequence Chart Studio: user-friendly drawing and verification tool for MSC.

Vojtěch ŘEHÁK, Matúš MADZIN, Ľuboš KORENČIAK, Petr GOTTHARD, Ondřej KOCIAN, Martin BEZDĚKA, Ondřej BOUDA, Václav VACEK, Milan MALOTA and Zuzana PEKARČÍKOVÁ.
URL

More details

publications.txt · Last modified: 2013/10/21 12:03 by Jan Obdrzalek