Christoph Haase : Publications

Directed Reachability for Infinite−State Systems

Michael Blondin‚ Christoph Haase and Philip Offtermatt

In Tools and Algorithms for the Construction and Analysis of Systems‚ TACAS. Springer. 2021.

To appear

Details about Directed Reachability for Infinite−State Systems | BibTeX data for Directed Reachability for Infinite−State Systems

On the Expressiveness of Büchi Arithmetic

Christoph Haase and Jakub Różycki

In Foundations of Software Science and Computation Structures‚ FOSSACS. Springer. 2021.

To appear

Details about On the Expressiveness of Büchi Arithmetic | BibTeX data for On the Expressiveness of Büchi Arithmetic

Approaching Arithmetic Theories with Finite−State Automata

Christoph Haase

In Language and Automata Theory and Applications‚ LATA. Vol. 12038 of Lect. Notes Comp. Sci.. Pages 1–11. Springer. 2020.

Details about Approaching Arithmetic Theories with Finite−State Automata | BibTeX data for Approaching Arithmetic Theories with Finite−State Automata | DOI (10.1007/978-3-030-40608-0_3)

On the power of ordering in linear arithmetic theories

Dmitry Chistikov and Christoph Haase

In Automata‚ Languages‚ and Programming‚ ICALP. Vol. 168 of LIPIcs. Pages 119:1–119:15. Schloss Dagstuhl − Leibniz−Zentrum fuer Informatik. 2020.

Details about On the power of ordering in linear arithmetic theories | BibTeX data for On the power of ordering in linear arithmetic theories | DOI (10.4230/LIPIcs.ICALP.2020.119)

On the Size of Finite Rational Matrix Semigroups

Georgina Bumpus‚ Christoph Haase‚ Stefan Kiefer‚ Paul−Ioan Stoienescu and Jonathan Tanner

In Automata‚ Languages‚ and Programming‚ ICALP. Vol. 168 of LIPIcs. Pages 115:1–115:13. Schloss Dagstuhl − Leibniz−Zentrum fuer Informatik. 2020.

Details about On the Size of Finite Rational Matrix Semigroups | BibTeX data for On the Size of Finite Rational Matrix Semigroups | DOI (10.4230/LIPIcs.ICALP.2020.115)

On the Existential Theories of Büchi Arithmetic and Linear p−adic Fields

Florent Guépin‚ Christoph Haase and James Worrell

In Logic in Computer Science‚ LICS. IEEE. 2019.

Details about On the Existential Theories of Büchi Arithmetic and Linear p−adic Fields | BibTeX data for On the Existential Theories of Büchi Arithmetic and Linear p−adic Fields | DOI (10.1109/LICS.2019.8785681)

Presburger arithmetic with stars‚ rational subsets of graph groups‚ and nested zero tests

Christoph Haase and Georg Zetzsche

In Logic in Computer Science‚ LICS. IEEE. 2019.

Details about Presburger arithmetic with stars‚ rational subsets of graph groups‚ and nested zero tests | BibTeX data for Presburger arithmetic with stars‚ rational subsets of graph groups‚ and nested zero tests | DOI (10.1109/LICS.2019.8785850)

Context−free commutative grammars with integer counters and resets

Dmitry Chistikov‚ Christoph Haase and Simon Halfon

In Theor. Comput. Sci.. Vol. 735. Pages 147–161. 2018.

Details about Context−free commutative grammars with integer counters and resets | BibTeX data for Context−free commutative grammars with integer counters and resets | DOI (10.1016/j.tcs.2016.06.017)

A survival guide to Presburger arithmetic

Christoph Haase

In SIGLOG News. Vol. 5. No. 3. Pages 67–82. 2018.

Details about A survival guide to Presburger arithmetic | BibTeX data for A survival guide to Presburger arithmetic | DOI (10.1145/3242953.3242964)

Affine Extensions of Integer Vector Addition Systems with States

Michael Blondin‚ Christoph Haase and Filip Mazowiecki

In Concurrency Theory‚ CONCUR. Vol. 118 of LIPIcs. Pages 14:1–14:17. Schloss Dagstuhl − Leibniz−Zentrum fuer Informatik. 2018.

Details about Affine Extensions of Integer Vector Addition Systems with States | BibTeX data for Affine Extensions of Integer Vector Addition Systems with States | DOI (10.4230/LIPIcs.CONCUR.2018.14)

The Logical View on Continuous Petri Nets

Michael Blondin‚ Alain Finkel‚ Christoph Haase and Serge Haddad

In ACM Trans. Comput. Log.. Vol. 18. No. 3. Pages 24:1–24:28. 2017.

Details about The Logical View on Continuous Petri Nets | BibTeX data for The Logical View on Continuous Petri Nets | DOI (10.1145/3105908)

Counting Problems for Parikh Images

Christoph Haase‚ Stefan Kiefer and Markus Lohrey

In Mathematical Foundations of Computer Science‚ MFCS. Vol. 83 of LIPIcs. Pages 12:1–12:13. Schloss Dagstuhl − Leibniz−Zentrum fuer Informatik. 2017.

Details about Counting Problems for Parikh Images | BibTeX data for Counting Problems for Parikh Images | DOI (10.4230/LIPIcs.MFCS.2017.12)

Logics for continuous reachability in Petri nets and vector addition systems with states

Michael Blondin and Christoph Haase

In Logic in Computer Science‚ LICS. IEEE. 2017.

Details about Logics for continuous reachability in Petri nets and vector addition systems with states | BibTeX data for Logics for continuous reachability in Petri nets and vector addition systems with states | DOI (10.1109/LICS.2017.8005068)

Computing quantiles in Markov chains with multi−dimensional costs

Christoph Haase‚ Stefan Kiefer and Markus Lohrey

In Logic in Computer Science‚ LICS. IEEE. 2017.

Details about Computing quantiles in Markov chains with multi−dimensional costs | BibTeX data for Computing quantiles in Markov chains with multi−dimensional costs | DOI (10.1109/LICS.2017.8005090)

On the Complexity of Quantified Integer Programming

Dmitry Chistikov and Christoph Haase

In Automata‚ Languages‚ and Programming‚ ICALP. Vol. 80 of LIPIcs. Pages 94:1–94:13. Schloss Dagstuhl − Leibniz−Zentrum fuer Informatik. 2017.

Details about On the Complexity of Quantified Integer Programming | BibTeX data for On the Complexity of Quantified Integer Programming | DOI (10.4230/LIPIcs.ICALP.2017.94)

Relating Reachability Problems in Timed and Counter Automata

Christoph Haase‚ Joël Ouaknine and James Worrell

In Fundam. Inform.. Vol. 143. No. 3−4. Pages 317–338. 2016.

Details about Relating Reachability Problems in Timed and Counter Automata | BibTeX data for Relating Reachability Problems in Timed and Counter Automata | DOI (10.3233/FI-2016-1316)

The complexity of the Kth largest subset problem and related problems

Christoph Haase and Stefan Kiefer

In Inf. Process. Lett.. Vol. 116. No. 2. Pages 111–115. 2016.

Details about The complexity of the Kth largest subset problem and related problems | BibTeX data for The complexity of the Kth largest subset problem and related problems | DOI (10.1016/j.ipl.2015.09.015)

A Polynomial−Time Algorithm for Reachability in Branching VASS in Dimension One

Stefan Göller‚ Christoph Haase‚ Ranko Lazic and Patrick Totzke

In Automata‚ Languages‚ and Programming‚ ICALP. Vol. 55 of LIPIcs. Pages 105:1–105:13. Schloss Dagstuhl − Leibniz−Zentrum fuer Informatik. 2016.

Details about A Polynomial−Time Algorithm for Reachability in Branching VASS in Dimension One | BibTeX data for A Polynomial−Time Algorithm for Reachability in Branching VASS in Dimension One | DOI (10.4230/LIPIcs.ICALP.2016.105)

Approaching the Coverability Problem Continuously

Michael Blondin‚ Alain Finkel‚ Christoph Haase and Serge Haddad

In Tools and Algorithms for the Construction and Analysis of Systems‚ TACAS. Vol. 9636 of Lect. Notes Comp. Sci.. Pages 480–496. Springer. 2016.

Details about Approaching the Coverability Problem Continuously | BibTeX data for Approaching the Coverability Problem Continuously | DOI (10.1007/978-3-662-49674-9\_28)

Tightening the Complexity of Equivalence Problems for Commutative Grammars

Christoph Haase and Piotr Hofman

In Symposium on Theoretical Aspects of Computer Science‚ STACS. Vol. 47 of LIPIcs. Pages 41:1–41:14. Schloss Dagstuhl − Leibniz−Zentrum fuer Informatik. 2016.

Details about Tightening the Complexity of Equivalence Problems for Commutative Grammars | BibTeX data for Tightening the Complexity of Equivalence Problems for Commutative Grammars | DOI (10.4230/LIPIcs.STACS.2016.41)

The Taming of the Semi−Linear Set

Dmitry Chistikov and Christoph Haase

In Automata‚ Languages‚ and Programming‚ ICALP. Vol. 55 of LIPIcs. Pages 128:1–128:13. Schloss Dagstuhl − Leibniz−Zentrum fuer Informatik. 2016.

Details about The Taming of the Semi−Linear Set | BibTeX data for The Taming of the Semi−Linear Set | DOI (10.4230/LIPIcs.ICALP.2016.128)

Reachability in Two−Dimensional Vector Addition Systems with States Is PSPACE−Complete

Michael Blondin‚ Alain Finkel‚ Stefan Göller‚ Christoph Haase and Pierre McKenzie

In Logic in Computer Science‚ LICS. Pages 32–43. IEEE. 2015.

Details about Reachability in Two−Dimensional Vector Addition Systems with States Is PSPACE−Complete | BibTeX data for Reachability in Two−Dimensional Vector Addition Systems with States Is PSPACE−Complete | DOI (10.1109/LICS.2015.14)

The Odds of Staying on Budget

Christoph Haase and Stefan Kiefer

In Automata‚ Languages‚ and Programming‚ ICALP. Vol. 9135 of Lect. Notes Comp. Sci.. Pages 234–246. Springer. 2015.

Details about The Odds of Staying on Budget | BibTeX data for The Odds of Staying on Budget | DOI (10.1007/978-3-662-47666-6\_19)

The Power of Priority Channel Systems

Christoph Haase‚ Sylvain Schmitz and Philippe Schnoebelen

In Log. Methods Comput. Sci.. Vol. 10. No. 4. 2014.

Details about The Power of Priority Channel Systems | BibTeX data for The Power of Priority Channel Systems | DOI (10.2168/LMCS-10(4:4)2014)

Integer Vector Addition Systems with States

Christoph Haase and Simon Halfon

In Reachability Problems‚ RP. Vol. 8762 of Lect. Notes Comp. Sci.. Pages 112–124. Springer. 2014.

Details about Integer Vector Addition Systems with States | BibTeX data for Integer Vector Addition Systems with States | DOI (10.1007/978-3-319-11439-2\_9)

Foundations for Decision Problems in Separation Logic with General Inductive Predicates

Timos Antonopoulos‚ Nikos Gorogiannis‚ Christoph Haase‚ Max I. Kanovich and Joël Ouaknine

In Foundations of Software Science and Computation Structures‚ FOSSACS. Vol. 8412 of Lect. Notes Comp. Sci.. Pages 411–425. Springer. 2014.

Details about Foundations for Decision Problems in Separation Logic with General Inductive Predicates | BibTeX data for Foundations for Decision Problems in Separation Logic with General Inductive Predicates | DOI (10.1007/978-3-642-54830-7\_27)

Subclasses of Presburger arithmetic and the weak EXP hierarchy

Christoph Haase

In Computer Science Logic and Logic in Computer Science‚ CSL−LICS. Pages 47:1–47:10. ACM. 2014.

Details about Subclasses of Presburger arithmetic and the weak EXP hierarchy | BibTeX data for Subclasses of Presburger arithmetic and the weak EXP hierarchy | DOI (10.1145/2603088.2603092)

Reachability in Register Machines with Polynomial Updates

Alain Finkel‚ Stefan Göller and Christoph Haase

In Mathematical Foundations of Computer Science‚ MFCS. Vol. 8087 of Lect. Notes Comp. Sci.. Pages 409–420. Springer. 2013.

Details about Reachability in Register Machines with Polynomial Updates | BibTeX data for Reachability in Register Machines with Polynomial Updates | DOI (10.1007/978-3-642-40313-2\_37)

The Power of Priority Channel Systems

Christoph Haase‚ Sylvain Schmitz and Philippe Schnoebelen

In Concurrency Theory‚ CONCUR. Vol. 8052 of Lect. Notes Comp. Sci.. Pages 319–333. Springer. 2013.

Details about The Power of Priority Channel Systems | BibTeX data for The Power of Priority Channel Systems | DOI (10.1007/978-3-642-40184-8\_23)

SeLoger: A Tool for Graph−Based Reasoning in Separation Logic

Christoph Haase‚ Samin Ishtiaq‚ Joël Ouaknine and Matthew J. Parkinson

In Computer Aided Verification‚ CAV. Vol. 8044 of Lect. Notes Comp. Sci.. Pages 790–795. Springer. 2013.

Details about SeLoger: A Tool for Graph−Based Reasoning in Separation Logic | BibTeX data for SeLoger: A Tool for Graph−Based Reasoning in Separation Logic | DOI (10.1007/978-3-642-39799-8\_55)

On the Relationship between Reachability Problems in Timed and Counter Automata

Christoph Haase‚ Joël Ouaknine and James Worrell

In Reachability Problems‚ RP. Vol. 7550 of Lect. Notes Comp. Sci.. Pages 54–65. Springer. 2012.

Details about On the Relationship between Reachability Problems in Timed and Counter Automata | BibTeX data for On the Relationship between Reachability Problems in Timed and Counter Automata | DOI (10.1007/978-3-642-33512-9\_6)

Branching−Time Model Checking of Parametric One−Counter Automata

Stefan Göller‚ Christoph Haase‚ Joël Ouaknine and James Worrell

In Foundations of Software Science and Computational Structures‚ FOSSACS. Vol. 7213 of Lect. Notes Comp. Sci.. Pages 406–420. Springer. 2012.

Details about Branching−Time Model Checking of Parametric One−Counter Automata | BibTeX data for Branching−Time Model Checking of Parametric One−Counter Automata | DOI (10.1007/978-3-642-28729-9\_27)

Tractable Reasoning in a Fragment of Separation Logic

Byron Cook‚ Christoph Haase‚ Joël Ouaknine‚ Matthew J. Parkinson and James Worrell

In Concurrency Theory‚ CONCUR. Vol. 6901 of Lect. Notes Comp. Sci.. Pages 235–249. Springer. 2011.

Details about Tractable Reasoning in a Fragment of Separation Logic | BibTeX data for Tractable Reasoning in a Fragment of Separation Logic | DOI (10.1007/978-3-642-23217-6\_16)

Model Checking Succinct and Parametric One−Counter Automata

Stefan Göller‚ Christoph Haase‚ Joël Ouaknine and James Worrell

In Automata‚ Languages and Programming‚ ICALP. Vol. 6199 of Lect. Notes Comp. Sci.. Pages 575–586. Springer. 2010.

Details about Model Checking Succinct and Parametric One−Counter Automata | BibTeX data for Model Checking Succinct and Parametric One−Counter Automata | DOI (10.1007/978-3-642-14162-1\_48)

On Process−Algebraic Extensions of Metric Temporal Logic

Christoph Haase‚ Joël Ouaknine and James Worrell

In Reflections on the Work of C. A. R. Hoare.. Pages 283–300. Springer. 2010.

Details about On Process−Algebraic Extensions of Metric Temporal Logic | BibTeX data for On Process−Algebraic Extensions of Metric Temporal Logic | DOI (10.1007/978-1-84882-912-1\_13)

Ideal Downward Refinement in the EL Description Logic

Jens Lehmann and Christoph Haase

In Inductive Logic Programming‚ ILP. Vol. 5989 of Lect. Notes Comp. Sci.. Pages 73–87. Springer. 2009.

Details about Ideal Downward Refinement in the EL Description Logic | BibTeX data for Ideal Downward Refinement in the EL Description Logic | DOI (10.1007/978-3-642-13840-9\_8) | Link to Ideal Downward Refinement in the EL Description Logic

Reachability in Succinct and Parametric One−Counter Automata

Christoph Haase‚ Stephan Kreutzer‚ Joël Ouaknine and James Worrell

In Concurrency Theory‚ CONCUR. Vol. 5710 of Lect. Notes Comp. Sci.. Pages 369–383. Springer. 2009.

Details about Reachability in Succinct and Parametric One−Counter Automata | BibTeX data for Reachability in Succinct and Parametric One−Counter Automata | DOI (10.1007/978-3-642-04081-8\_25)

Complexity of Subsumption in the EL Family of Description Logics: Acyclic and Cyclic TBoxes

Christoph Haase and Carsten Lutz

In European Conference on Artificial Intelligence‚ ECAI. Vol. 178 of Frontiers in Artificial Intelligence and Applications. Pages 25–29. IOS Press. 2008.

Details about Complexity of Subsumption in the EL Family of Description Logics: Acyclic and Cyclic TBoxes | BibTeX data for Complexity of Subsumption in the EL Family of Description Logics: Acyclic and Cyclic TBoxes | DOI (10.3233/978-1-58603-891-5-25)