Home Projects Publications Activities
Text books
Edited volumes
Journal papers
Book contributions
Conference papers
Workshop papers
Unrefereed publications
Submitted papers
Preprints and Notes
Dissertations

Text books

[T2] S. Demri, V. Goranko, M. Lange
Temporal Logics in Computer Science (Finite-State Systems)
Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2016, ~750 pages, ISBN 9781107028364
web page
[T1] M. Hofmann, M. Lange
Automatentheorie und Logik
eXamen.press, Spinger, 2011, 240 pages, ISBN 978-3-642-18089-7
web page


Edited volumes

[E4] C. Draude, M. Lange, B. Sick
INFORMATIK 2019: 50 Jahre Gesellschaft für Informatik - Informatik für Gesellschaft
Workshopbeiträge, LNI P-295, GI 2019
[E3] K. David, K. Geihs, M. Lange, G. Stumme
INFORMATIK 2019: 50 Jahre Gesellschaft für Informatik - Informatik für Gesellschaft
Konferenzbeiträge, LNI P-294, GI 2019
[E2] F. Grandi, M. Lange, A. Lomuscio
22nd International Symposium on Temporal Representation and Reasoning (TIME 2015)
special issue, Information and Computation 259(3), Elsevier, 2018
[E1] F. Grandi, M. Lange, A. Lomuscio
22nd International Symposium on Temporal Representation and Reasoning (TIME 2015)
IEEE Computer Society, 2015


Journal papers

[J36] F. Bruse, M. Lange
Model Checking Timed Recursive CTL
Information and Computation 298:105168, 2024
[J35] F. Bruse, M. Herwig, M. Lange
Weights of Formal Languages Based on Geometric Series with an Application to Automatic Grading
Theoretical Computer Science 938:114295, 2023
[J34] M. Sälzer, M. Lange
Reachability in Simple Neural Networks
Fundamenta Informaticae, 189(3-4):241-259, special issue on RP'21, 2023
DOI, arXiv
[J33] F. Bruse, M. Lange, E. Lozes
The Tail-Recursive Fragment of Timed Recursive CTL
Information and Computation, 294:105084, special issue on TIME'22, 2023
DOI
[J32] F. Bruse, J. Kreiker, M. Lange, M. Sälzer
Local Higher-Order Fixpoint Iteration
Information and Computation 289(B):104963, special issue on GandALF'20, 2022
[J31] F. Bruse, M. Lange
Temporal Logic with Recursion
Information and Computation 281:104804, special issue on TIME'20, 2021
[J30] F. Bruse, M. Lange, E. Lozes
The Complexity of Model Checking Tail-Recursive Higher-Order Fixpoint Logic
Fundamenta Informaticae 178(1-2):1-30, 2021
[J29] D. Kernberger, M. Lange
On the Expressive Power of Hybrid Branching-Time Logics
Theoretical Computer Science 813:362-374, 2020
[J28] D. Kernberger, M. Lange
Model Checking for Hybrid Branching-Time Logics
Journal of Logic and Algebraic Programming 110, special issue on TIME'16, 2020
[J27] M. Hutagalung, N. Hundeshagen, D. Kuske, M. Lange, E. Lozes
Multi-Buffer Simulations: Decidability and Complexity
Information and Computation 262(2):280-310, special issue on GandALF'16, 2018
Abstract
[J26] O. Friedmann, F. Klaedtke, M. Lange
Ramsey-based Inclusion Checking for Visibly Pushdown Automata
ACM Transactions on Computational Logic 16(4):34.1-34.24, 2015
Abstract
[J25] F. Bruse, O. Friedmann, M. Lange
On Guarded Transformation in the Modal μ-Calculus
Logic Journal of the IGPL 23(2):194-216, 2015
Abstract
[J24] M. Lange, E. Lozes, M. Vargas Guzman
Model Checking Process Equivalences
Theoretical Computer Science 560(3):326-347, special issue on GandALF'12, 2014
Abstract
[J23] J. Gutierrez, F. Klaedtke, M. Lange
The μ-Calculus Alternation Hierarchy Collapses over Structures with Bounded Connectivity
Theoretical Computer Science 560(3):292-306, special issue on GandALF'12, 2014
Abstract
[J22] O. Friedmann, M. Lange
Deciding the Unguarded Modal μ-Calculus
Journal of Applied Non-Classical Logics 23(4):353-371, 2013
Abstract
[J21] O. Friedmann, M. Latte, M. Lange
Satisfiability Games for Branching-Time Logics
Logical Methods in Computer Science 9(4:5), 2013
Abstract
[J20] M. Latte, M. Lange
Branching-Time Logics with Path Relativisation
Journal of Computer and System Sciences 80(2):375-389, special issue on WoLLIC'10, 2014
Abstract, preprint PDF, full paper (© Elsevier)
[J19] K. Heljanko, M. Keinänen, M. Lange, I. Niemelä
Solving Parity Games by a Reduction to SAT
Journal of Computer and System Sciences 78(2):430-440, special issue on Games in Verification, 2012
Abstract
[J18] O. Friedmann, M. Lange
Two Local Strategy Improvement Schemes for Parity Game Solving
Journal of Foundations of Computer Science 23(3):669-685, special issue on GandALF'10, 2011
Abstract
[J17] M. Lange
P-Hardness of the Emptiness Problem for Visibly Pushdown Languages
Information Processing Letters 111(7):338-341, 2011
Abstract, preprint PDF, full paper (© Elsevier)
[J16] O. Friedmann, M. Lange
More on Balanced Diets
Journal of Functional Programming 21(2):135-157, 2011
Abstract
[J15] C. Dax, F. Klaedtke, M. Lange
On Regular Temporal Logics with Past
Acta Informatica 47(4):251-277, 2010
Abstract
[J14] M. Lange, H. Leiß
To CNF or not to CNF? An Efficient Yet Presentable Version of the CYK Algorithm
Informatica Didactica 8, 2009
Abstract, online version
[J13] M. Lange
Model Checking for Hybrid Logic
Journal of Logic, Language and Information 18(4):465-491, special issue on Hybrid Logic, 2009
Abstract
[J12] A. Søgaard, M. Lange
Polyadic Dynamic Logics for HPSG Parsing
Journal of Logic, Language and Information 18(2):159-198, 2009
Abstract
[J11] M. Lange
A Purely Model-Theoretic Proof of the Exponential Succinctness Gap between CTL+ and CTL
Information Processing Letters 108:308-312, 2008
Abstract, PDF (© Elsevier)
[J10] K. Brünnler, M. Lange
Cut-Free Sequent Systems for Temporal Logic
Journal of Logic and Algebraic Programming 76(2):216-225, 2008
Abstract
[J9] R. Axelsson, M. Lange, R. Somla
The Complexity of Model Checking Higher-Order Fixpoint Logic
Logical Methods in Computer Science 3(2:7):1-33, 2007
Abstract, PDF
[J8] O. Grumberg, M. Lange, M. Leucker, S. Shoham
When Not Losing Is Better than Winning: Abstraction and Refinement for the Full μ-Calculus
Information and Computation 205(8):1130-1148, 2007
Abstract, PDF (© Elsevier)
[J7] M. Lange
Three Notes on the Complexity of Model Checking Fixpoint Logic with Chop
RAIRO - Theoretical Informatics and Applications 41:177-190, 2007
Abstract, PDF (© EDP Sciences; the original publication is available at www.edpsciences.org/ita.)
[J6] M. Lange
The Alternation Hierarchy in Fixpoint Logic with Chop Is Strict Too
Information and Computation 204(9):1346-1367, 2006
Abstract, PDF (© Elsevier)
[J5] M. Lange, R. Somla
Propositional Dynamic Logic of Context-Free Programs and Fixpoint Logic with Chop
Information Processing Letters 100(2):72-75, 2006.
Abstract, PDF (© Elsevier)
[J4] M. Lange, C. Lutz
2-ExpTime Lower Bounds for Propositional Dynamic Logics with Intersection
Journal of Symbolic Logic 70(4):1072-1086, 2005.
Abstract
[J3] M. Lange
Model Checking Propositional Dynamic Logic with All Extras
Journal of Applied Logic 4(1):39-49, 2005.
Abstract, PDF (© Elsevier)
[J2] M. Lange
A Quick Axiomatisation of LTL with Past
Mathematical Logic Quarterly 51(1):83-88, 2005
Abstract
[J1] M. Lange, C. Stirling
Model Checking Games for Branching Time Logics
Journal of Logic and Computation 12(4):623-639, special issue on ICTL'00, 2002
Abstract, PDF (© Oxford University Press)


Book contributions

[B4] M. Kastaun, M. Meier, N. Hundeshagen, M. Lange
ProfiLL: Professionalisierung durch intelligente Lehr-Lernsysteme
In Bildung, Schule, Digitalisierung, Waxmann-Verlag, 2020
[B3] S. Kreutzer, M. Lange
Non-Regular Fixed-Point Logics and Games
In J. Flum, E. Grädel, T. Wilke (eds.), Logic and Automata: History and Perspectives, vol. 2 of Texts in Logic and Games, pages 433-466, Amsterdam University Press, 2007
Abstract
[B2] M. Lange
A Lower Complexity Bound for Propositional Dynamic Logic with Intersection
In Advances in Modal Logic Volume 5, pages 133-147, 2005, King`s College Publications
Abstract
[B1] M. Lange, M. Leucker, T. Noll, S. Tobies
Truth - a Verification Platform for Concurrent Systems
In Tool Support for System Specification, Development, and Verification, Advances in Computing Science. Springer-Verlag Wien New York, 1999.
Abstract


Conference papers

[C63] F. Bruse, M. Lange
Computing All Minimal Ways to Reach a Context-Free Language
To appear in Proc. of the 18th Int. Conference on Reachability Problems, RP'24, Vienna, A, 2024
vol. ?? of Lecture Notes in Computer Science, pages ??-??, Springer
[C62] M. Herwig, N. Hundeshagen, J. Hundhausen, S. Kablowski, M. Lange
Problem-Specific Visual Feedback in Discrete Modelling
In Proc. 22. Fachtagung Bildungstechnologien, DELFI'24, Fulda, D, 2024
vol. P356 of Lecture Notes in Informatics, Gesellschaft für Informatik
DOI
[C61] M. Sälzer, E. Alsmann, F. Bruse, M. Lange
Verifying And Interpreting Neural Networks using Finite Automata
In Proc. of the 28th Int. Conf. on Developments in Language Theory, DLT'24, Göttingen, D, 2024
vol. 14791 of Lecture Notes in Computer Science, pages 266-281, Springer
[C60] F. Bruse, M. Kastaun, M. Lange, S. Möller
The Calculus of Temporal Influence
In Proc. of the 30th Int. Symp. on Temporal Representation and Reasoning, TIME'23, Athens, GR, 2023
vol. 278 of LIPIcs, pages 10:1-10:19
[C59] F. Bruse, M. Lange, S. Möller
Formal Reasoning about Influence in Natural Sciences Experiments
In Proc. of the 29th Int. Conf. on Automated Deduction, CADE'23, Rome, IT, 2023
vol. 14132 of Lecture Notes in Computer Science, pages 153-169, Springer
[C58] M. Sälzer, M. Lange
Fundamental Limits in Formal Verification of Message-Passing Neural Networks
In Proc. of the 11th Int. Conf. on Learning Representations, ICLR'23 , Kigali, RWA, 2023
OpenReview.net, 2023
Link
[C57] F. Bruse, D. Kronenberger, M. Lange
Capturing Bisimulation-Invariant Time-Complexity Classes via Polyadic Higher-Order Fixpoint Logic
In Proc. of the 13th Int. Symp. on Games, Automata, Logics and Formal Verification, Gandalf'22, Madrid, E, 2022
vol. 370 of Elect. Proc. in Theor. Computer Science, pages 17-33
[C56] F. Bruse, M. Lange, E. Lozes
The Tail-Recursive Fragment of Timed Recursive CTL
In Proc. of the 29th Int. Symp. on Temporal Representation and Reasoning, TIME'22, online, 2022
vol. 247 of LIPIcs, pages 5:1-5:16
[C55] F. Bruse, M. Herwig, M. Lange
A Similarity Measure for Formal Languages Based on Convergent Geometric Series
In Proc. of the 26th Int. Conference on Implementation and Application of Automata, CIAA'22, Rouen, F, 2022
vol. 13266 of Lecture Notes in Computer Science, pages 80-92, Springer
[C54] M. Sälzer, M. Lange
Reachability Is NP-Complete Even for the Simplest Neural Networks
In Proc. of the 15th Int. Conference on Reachability Problems, RP'21, Liverpool, UK, 2021
vol. 13035 of Lecture Notes in Computer Science, pages 149-164, Springer
Abstract
[C53] F. Bruse, M. Lange, M. Sälzer
Finite Convergence of Mu-Calculus Fixpoints on Genuinely Infinite Structures
In Proc. of 46th Int. Symp. on Mathematical Foundations of Computer Science, MFCS'21, Tallin, EE, 2021
vol. 202 of LIPIcs, pages 24:1-24:19
Link
[C52] F. Bruse, M. Lange
Model Checking Timed Recursive CTL
In Proc. of the 28th Int. Symp. on Temporal Representation and Reasoning, TIME'21, Klagenfurt, A, 2021
vol. 206 of LIPIcs, pages 12:1-12:14
Link
[C51] F. Bruse, M. Lange
A Decidable Non-Regular Modal Fixpoint Logic
To appear in Proc. of the 32nd Int. Conf. on Concurrency Theory, CONCUR'21, Paris, F, 2021
vol. 203 of LIPIcs, pages 23:1-23:18
Link
[C50] N. Hundeshagen, M. Lange, G. Siebert
DiMo - Discrete Modelling Using Propositional Logic
In Proc. of the 24th Int. Conf. on Theory and Applications of Satisfiability Testing, SAT'21, Barcelona, ES, 2021
vol. 12831 of Lecture Notes in Computer Science, pages 242-250, Springer
Abstract
[C49] F. Bruse, J. Kreiker, M. Lange, M. Sälzer
Local Higher-Order Fixpoint Iteration
In Proc. of the 11th Int. Symp. on Games, Automata, Logics and Formal Verification, Gandalf'20, Brussels, BE, 2020
vol. 326 of Elect. Proc. in Theor. Computer Science, pages 97-113
Link
[C48] F. Bruse, M. Lange
Temporal Logic with Recursion
In Proc. of the 27th Int. Symp. on Temporal Representation and Reasoning, TIME'20, Bozen, IT, 2020
vol. 178 of LIPIcs, pages 6:1-6:14
Link
[C47] P. Gawrychowski, M. Lange, N. Rampersad, J. Shallit, M. Szykuła
Existential Length Universality
In Proc. of the 37th Symp. on Theoretical Aspects of Computer Science, STACS'20, Montpellier, F, 2020
vol. 154 of LIPIcs, pages 16:1-16:14
Link
[C46] C. Eickhoff, M. Lange, S.-L. Raesch, A. Zündorf
EMFeR: Model Checking for Object Oriented (EMF) Models
In Proc. of the 7th Int. Conf. on Model-Driven Engineering and Software Development, MODELSWARD'19, Prague, CZ, 2019
SciTePress 2019, pages 511-518
Link
[C45] D. Kernberger, M. Lange
On the Expressive Power of Hybrid Branching-Time Logics
In Proc. of the 25th Int. Symp. on Temporal Representation and Reasoning, TIME'18, Warsaw, PL, 2018
vol. 120 of LIPIcs, pages 16:1-16:18
Link
[C44] D. Kernberger, M. Lange
The Fully Hybrid μ-Calculus
In Proc. of the 24th Int. Symp. on Temporal Representation and Reasoning, TIME'17, Mons, BE, 2017
vol. 90 of LIPIcs, pages 17:1-17:16
Link
[C43] N. Hundeshagen, M. Lange
Model Checking CTL Over Restricted Classes of Automatic Structures
In Proc. of the 11th Int. Workshop on Reachability Problems, RP'17, Egham, UK, 2017
vol. 10506 of Lecture Notes in Computer Science, pages 87-100, Springer
Abstract, PDF
[C42] F. Bruse, M. Lange, E. Lozes
Space-Efficient Fragments of Higher-Order Fixpoint Logic
In Proc. of the 11th Int. Workshop on Reachability Problems, RP'17, Egham, UK , 2017
vol. 10506 of Lecture Notes in Computer Science, pages 26-41, Springer
Abstract, PDF
[C41] D. Kernberger, M. Lange
Model Checking for the Full Hybrid Computation Tree Logic
In Proc. of the 23rd Int. Symp. on Temporal Representation and Reasoning, TIME'16, Copenhagen, DK, 2016
IEEE Computer Society
Abstract, PDF
[C40] M. Hutagalung, N. Hundeshagen, D. Kuske, M. Lange, E. Lozes
Multi-Buffer Simulations for Trace Language Inclusion
In Proc. of the 7th Int. Symp. on Games, Automata, Logics and Formal Verification, Gandalf'16, Catania, IT, 2016
vol. 226 of Elect. Proc. in Theor. Computer Science, pages 120-134
Abstract, Link
[C39] F. Bruse, D. Kernberger, M. Lange
A Canonical Model Construction for Iteration-Free PDL with Intersection
In Proc. of the 7th Int. Symp. on Games, Automata, Logics and Formal Verification, Gandalf'16, Catania, IT, 2016
vol. 226 of Elect. Proc. in Theor. Computer Science, pages 213-227
Abstract, Link
[C38] M. Lange, E. Lozes
Conjunctive Visibly-Pushdown Path Queries
In Proc. of 20th Int. Symp. on Fundamentals of Computation Theory, FCT'15, Gdansk, PL, 2015
vol. 9210 of Lecture Notes in Computer Science, pages 327-338, Springer
Abstract, PDF
[C37] A. Ehle, N. Hundeshagen, M. Lange
The Sequent Calculus Trainer - Helping Students to Correctly Construct Proofs
In Proc. of the 4th Int. Conf. on Tools for Teaching Logic, TTL'15, Rennes, FR, 2015
Abstract, PDF
[C36] F. Bruse, M. Falk, M. Lange
The Fixpoint-Iteration Algorithm for Parity Games
In Proc. of the 5th Int. Symp. on Games, Automata, Logics and Formal Verification, Gandalf'14, Verona, IT, 2014
vol. 161 of Elect. Proc. in Theor. Computer Science, pages 116-130
Abstract, Link
[C35] M. Lange, E. Lozes
Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic
In Proc. of the 8th IFIP Int. Conf. on Theoretical Computer Science, TCS'14, Rome, IT, 2014
vol. 8705 of Lecture Notes in Computer Science, pages 90-103, Springer
Abstract, PDF
[C34] M. Hutagalung, M. Lange, E. Lozes
Buffered Simulation Games for Büchi Automata
In Proc. of the 14th Int. Conf. on Automata and Formal Languages, AFL'14, Szeged, H, 2014
vol. 151 of Elect. Proc. in Theor. Computer Science, pages 286-300
Abstract, Link
[C33] R. Ehlers, M. Lange
A Tool that Incrementally Approximates the Finite Satisfiability Problem for Full Interval Temporal Logic
In Proc. of the 7th Int. Joint Conf. on Automated Reasoning, IJCAR'14, Vienna, A, 2014
vol. 8562 of Lecture Notes in Computer Science, pages 360-366, Springer
Abstract, PDF
[C32] M. Hutagalung, M. Lange
Model Checking for String Problems
In Proc. of the 9th Int. Computer Science Symp. in Russia, CSR'14, Moscow, RU, 2014
vol. 8476 of Lecture Notes in Computer Science, pages 190-203, Springer
Abstract, PDF
[C31] O. Friedmann, F. Klaedtke, M. Lange
Ramsey Goes Visibly Pushdown
In Proc. of the 40th Int. Coll. on Algorithms, Languages and Programming, ICALP'13, Riga, LV, 2013
vol. 7966 of Lecture Notes in Computer Science, pages 224-237, Springer
Abstract, PDF (long version with proof details)
[C30] M. Hutagalung, M. Lange, E. Lozes
Revealing vs. Concealing: More Simulation Games for Büchi Inclusion
In Proc. of the 7th Int. Conf. on Language and Automata Theory and Applications, LATA'13, Bilbao, ES, 2013
vol. 7810 of Lecture Notes in Computer Science, pages 347-358, Springer
Abstract, PDF
[C29] J. Gutierrez, F. Klaedtke, M. Lange
The μ-Calculus Alternation Hierarchy Collapses over Structures with Bounded Connectivity
In Proc. of the 3rd Symp. on Games, Automata, Logics and Formal Verification, GandALF'12, Napoli, IT, 2012
vol. 96 of Electr. Proc. in Theor. Comp. Sc., pages 113-126
Abstract, PDF
[C28] M. Lange, E. Lozes, M. Vargas Guzman
Model Checking Process Equivalences
In Proc. of the 3rd Symp. on Games, Automata, Logics and Formal Verification, GandALF'12, Napoli, IT, 2012
vol. 96 of Electr. Proc. in Theor. Comp. Sc., pages 43-56
Abstract, Link
[C27] M. Latte, M. Lange
Branching Time? Pruning Time!
In Proc. of the 6th Int. Joint Conf. on Automated Reasoning, IJCAR'12, Manchester, UK, 2012
vol. 7364 of Lecture Notes in Computer Science, pages 393-407, Springer
Abstract, PDF (© Springer-Verlag)
[C26] O. Friedmann, M. Lange
Ramsey-Based Analysis of Parity Automata
In Proc. of the 18th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'12, Tallinn, EST, 2012
vol. 7214 of Lecture Notes in Computer Science, pages 64-78, Springer
Abstract, PDF (© Springer-Verlag)
[C25] B. Badban, M. Lange
Exact Incremental Analysis of Timed Automata Using an SMT Solver
In Proc. of the 9th Int. Conf. on Formal Modeling and Analysis of Timed Systems, FORMATS'11, Aalborg, DK, 2011
vol. 6919 of Lecture Notes in Computer Science, pages 177-192, Springer
Abstract, PDF (© Springer-Verlag)
[C24] R. Axelsson, M. Lange
Formal Language Constrained Reachability and Model Checking Propositional Dynamic Logics
In Proc. of the 5th Workshop on Reachability Problems, RP'11, Genova, Italy, 2011,
volume 6945 of Lecture Notes in Computer Science, pages 45-57,
Abstract, PDF (© Springer-Verlag)
[C23] O. Friedmann, M. Lange
The Modal μ-Calculus Caught Off Guard
In Proc. of the 20th Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX'11, Bern, CH, 2011
volume 6793 of Lecture Notes in Artificial Intelligence, pages 149-163, Springer
Abstract, PDF (© Springer-Verlag)
[C22] R. Axelsson, M. Hague, S. Kreutzer, M. Lange, M. Latte
Extended Computation Tree Logic
In Proc. of the 17th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-17, Yogyakarta, RI, 2010
volume 6397 of Lecture Notes in Computer Science, pages 67-81
Abstract, PDF (© Springer-Verlag)
[C21] O. Friedmann, M. Lange
Local Strategy Improvement for Parity Game Solving
In Proc. of the 1st Int. Symp. on Games, Automata, Logics and Formal Verification, GandALF'10, Minori, IT, 2010
volume 25 of Electronic Notes in Theoretical Computer Science, pages 118-131
Abstract, PDF
[C20] O. Friedmann, M. Latte, M. Lange
A Decision Procedure for CTL* Based on Tableaux and Automata
In Proc. of the 5th Int. Joint Conference on Automated Reasoning, IJCAR'10, Edinburgh, UK, 2010
volume 6173 of Lecture Notes in Artificial Intelligence, pages 331-345
Abstract, PDF (© Springer-Verlag)
[C19] O. Friedmann, M. Lange
Solving Parity Games in Practice
In Proc. of the 7th Int. Symp. on Automated Technology for Verification and Analysis, ATVA'09, Macao, China, 2009
volume 5799 of Lecture Notes in Computer Science, pages 182-196
Abstract, PDF (© Springer-Verlag)
[C18] A. Kara, V. Weber, M. Lange, T. Schwentick
On the Hybrid Extension of CTL and CTL+
In Proc. of the 34th Int. Symp. on Mathematical Foundations of Computer Science, MFCS'09, Novy Smokovec, Slovakia, 2009
volume 5734 of Lecture Notes in Computer Science, pages 427-438
Abstract, PDF (© Springer-Verlag)
[C17] C. Dax, F. Klaedtke, M. Lange
On Regular Temporal Logics with Past Operators
In Proc. of the 36th Int. Coll. on Automata, Languages and Programming, ICALP'09, Rhodes Island, Greece, 2009
volume 5556 of Lecture Notes in Computer Science, pages 175-187, © Springer-Verlag
Abstract, PDF (© Springer-Verlag)
[C16] R. Axelsson, K. Heljanko, M. Lange
Analyzing Context-Free Grammars Using an Incremental SAT Solver
In Proc. of the 35th Int. Coll. on Automata, Languages and Programming, ICALP'08, Reykjavik, Iceland, 2008
volume 5126 of Lecture Notes in Computer Science, pages 410-422
Abstract, PDF (© Springer-Verlag)
[C15] R. Axelsson, M. Lange
Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic
In Proc. of the 14th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'07, Yerevan, Armenia, 2007,
volume 4790 of Lecture Notes in Computer Science, pages 62-76
Abstract, PDF (© Springer-Verlag)
[C14] M. Lange
Linear Time Logics around PSL: Complexity, Expressiveness, and a little bit of Succinctness
In Proc. of the 18th Int. Conf. on Concurrency Theory, CONCUR'07, Lisbon, Portugal, 2007
volume 4703 of Lecture Notes in Computer Science, pages 90-104
Abstract, PDF (© Springer-Verlag)
[C13] C. Dax, M. Hofmann, M. Lange
A Proof System for the Linear Time μ-Calculus
In Proc. of the 26th Conf. on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'06, Kolkata, India, 2006
volume 4337 of Lecture Notes in Computer Science, pages 274-285
Abstract, PDF (© Springer-Verlag)
[C12] K. Heljanko, T. Junttila, M. Keinänen, M. Lange, T. Latvala
Bounded Model Checking for Weak Alternating Büchi Automata
In Proc. of the 18th Int. Conf. on Computer Aided Verification, CAV'06, Seattle, WA, USA, 2006
volume 4144 of Lecture Notes in Computer Science, pages 95-108
Abstract, PDF (© Springer-Verlag)
[C11] M. Lange, R. Somla
The Complexity of Model Checking Higher Order Fixpoint Logic
In Proc. of 30th Int. Symp. on Mathematical Foundations of Computer Science, MFCS'05, Gdansk, Poland, 2005
volume 3618 of Lecture Notes in Computer Science, pages 640-651
Abstract, PDF (© Springer-Verlag)
[C10] M. Lange
Weak Automata for the Linear Time μ-Calculus
In Proc. of the 6th Int. Conference on Verification, Model Checking and Abstract Interpretation, VMCAI'05, Paris, France, 2005
volume 3385 of Lecture Notes in Computer Science, pages 267-281
Abstract, PDF (© Springer-Verlag)
[C9] O. Grumberg, M. Lange, M. Leucker, S. Shoham
Don't Know in the μ-Calculus
In Proc. of the 6th Int. Conference on Verification, Model Checking and Abstract Interpretation, VMCAI'05, Paris, France, 2005
volume 3385 of Lecture Notes in Computer Science, pages 233-249
Abstract, PDF (© Springer-Verlag)
[C8] M. Lange
A Lower Complexity Bound for Propositional Dynamic Logic with Intersection
In Proc. of Advances in Modal Logic 2004, AiML'04, Manchester, UK, 2004
University of Manchester Technical Report UMCS-04-09-01
Abstract, PDF
[C7] M. Lange
Symbolic Model Checking of Non-Regular Properties
In Proc. of the 16th Int. Conf. on Computer Aided Verification, CAV'04, Boston, MA, USA, 2004
volume 3114 of Lecture Notes in Computer Science, pages 83-95
Abstract, Disclaimer
[C6] M. Lange
Satisfiability and Completeness of Converse-PDL Replayed
In Proc. of the 26th German Conference on Artificial Intelligence, KI'03, Hamburg, Germany, 2003
volume 2821 of Lecture Notes in Artificial Intelligence, pages 79-92
Abstract, PDF (© Springer-Verlag)
[C5] J. Johannsen, M. Lange
CTL+ is Complete for Double Exponential Time
In Proc. of the 30th Int. Colloquium on Automata, Languages and Programming, ICALP'03, Eindhoven, The Netherlands, 2003
volume 2719 of Lecture Notes in Computer Science, pages 767-775
Abstract, PDF (© Springer-Verlag)
[C4] M. Lange
Local Model Checking Games for Fixed Point Logic with Chop
In Proc. of the 13th International Conference on Concurrency Theory, CONCUR'02, Brno, Czech Republic, 2002
volume 2421 of Lecture Notes in Computer Science, pages 240-254
Abstract, PDF (© Springer-Verlag)
[C3] M. Lange, C. Stirling
Model Checking Fixed Point Logic with Chop
In Proc. of Foundations of Software Science and Computation Structures, FOSSACS'02, Grenoble, France, 2002
volume 2303 of Lecture Notes in Computer Science, pages 250-263
Abstract, PDF (© Springer-Verlag)
[C2] M. Lange, C. Stirling
Focus Games for Satisfiability and Completeness of Temporal Logic
In Proc. of the 16th Annual IEEE Symposium on Logic in Computer Science, LICS'01, Boston, MA, USA, 2001
Abstract, PDF
[C1] M. Lange, C. Stirling
Model Checking Games for CTL*
In Proc. of the International Conference on Temporal Logic, ICTL'2000, Leipzig, Germany, 2000
Abstract, PDF


Workshop papers

[W19] M. Sälzer, E. Alsmann, M. Lange
On Challenges and Opportunities in the Translation of Deep Neural Networks into Finite Automata
In Proc. of the 5th Workshop on Artificial Intelligence and formal Verification, Logic, Automata, and Synthesis, OVERLAY'23, Rome, IT, 2023
[W18] M. Herwig, N. Hundeshagen, M. Lange
Towards Graphical Feedback in the DiMo Learning Tool
Accepted for presentation at Formal Methods Education Online: Tips, Tricks & Tools, FOMEO'22, Haifa, IL, 2022
[W17] N. Hundeshagen, M. Lange
A Proposal for a Framework to Accompany Learning Tools
In Proc. of the Formal Methods Teaching Workshop and Tutorial, FMTea'21, Beijing, CN, 2021
vol. 13122 of Lecture Notes in Computer Science, pp. 35-42, Springer
[W16] E. Alsmann, F. Bruse, M. Lange
Separating the Expressive Power of Propositional Dynamic and Modal Fixpoint Logics
In Proceedings of the Combined 28th Int. Workshop on Expressiveness in Concurrency and 18th Workshop on Structural Operational Semantics, EXPRESS/SOS'21, Paris, F, 2021
vol. 339 of Electr. Proc. in Theor. Comp. Science, pp. 10-26
Link
[W15] F. Bruse, M. Lange, E. Lozes
Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic
Workshop on Programming and Reasoning on Infinite Structures, PARIS'14, Oxford, UK, 2018
Paper
[W14] A. Ehle, N. Hundeshagen, M. Lange
The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs
In Proc. of the Workshop on Theorem Proving Components for Educational Software, ThEdu'17, Gothenburg, S, 2017,
volume 267 of Electronic Proceedings in Theoretical Computer Science, pages 19-37
Abstract, Link
[W13] M. Hutagalung, N. Hundeshagen, D. Kuske, M. Lange, E. Lozes
Two-Buffer Simulation Games
In Proc. of the CASSTING'16 Workshop, Eindhoven, NL, 2016
volume 220 of Electronic Proceedings in Theoretical Computer Science, pages 27-38
Abstract Link
[W12] M. Lange
The Arity Hierarchy in the Polyadic μ-Calculus
In Proc. of the 11th Workshop on Fixpoints in Computer Science, FICS'15, Berlin, Germany, 2015
volume 191 of Electronic Proceedings in Theoretical Computer Science, pages 105-116
Abstract, Link
[W11] M. Lange, E. Lozes
Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic (Extended Abstract)
Workshop on Logic and Computational Complexity, LCC'14, Vienna, A, 2014
Abstract
[W10] M. Lange, E. Lozes
Model Checking the Higher-Dimensional Modal μ-Calculus
In Proc. of the 8th Workshop on Fixpoints in Computer Science, FICS'12, Tallinn, Estonia, 2012
volume 77 of Electronic Proceedings in Theoretical Computer Science, pages 39-46
Abstract, PDF
[W9] O. Friedmann, M. Lange
A Solver for Modal Fixpoint Logics
In Proc. of the 6th Workshop on Methods for Modalities, M4M-6, Copenhagen, Denmark, 2009
vol. 262 of Electr. Notes in Theor. Computer Science, pp. 99-111, Elsevier
Abstract, PDF
[W8] S. Kreutzer, M. Lange
A Note on the Relation between Inflationary Fixpoints and Least Fixpoints of Higher-Order
In Proc. of the 6th Workshop on Fixed Points in Computer Science, FICS'09, Coimbra, Portugal, 2009
Abstract, PDF
[W7] M. Lange
Solving Parity Games by a Reduction to SAT
In Proc. of the Workshop on Games in Design and Verification, GDV'05, Edinburgh, Scotland, UK, 2005
Abstract, PDF
[W6] M. Jehle, J. Johannsen, M. Lange, N. Rachinsky
Bounded Model Checking for All Regular Properties
In Proc. of the 3rd Int. Workshop on Bounded Model Checking, BMC'05, Edinburgh, Scotland, UK, 2005
volume 144.1 of Elect. Notes in Theor. Comp. Science, pages 3-18, Elsevier Science, 2005
Abstract, PDF
[W5] M. Lange, H. W. Loidl
Parallel and Symbolic Model Checking for Fixpoint Logic with Chop
In Proc. of the 3rd Int. Workshop on Parallel and Distributed Methods in Verification, PDMC'04, London, UK,
volume 128.3 of Elect. Notes in Theor. Comp. Science, pages 125-138, Elsevier Science, 2005
Abstract, PDF
[W4] C. Dax, M. Lange
Game Over: The Foci Approach to LTL Satisfiability and Model Checking
In Proc. of the Workshop on Games in Design and Verification, GDV'04, Boston, MA, USA,
volume 119.1 of Elect. Notes in Theor. Comp. Science, pages 33-49, Elsevier Science, 2005
Abstract, PDF
[W3] M. Lange
Alternating Context-Free Languages and Linear Time μ-Calculus with Sequential Composition
In Proceedings of the 9th Int. Workshop on Expressiveness in Concurrency, EXPRESS'02, Brno, Czech Republic, 2002
volume 68.2 of Electr. Notes in Theor. Comp. Science, Elsevier Science
Abstract, PDF
[W2] M. Lange
A Game Based Approach to CTL* Model Checking
In Proceedings of the summer school MOVEP'2k, Nantes, France, 2000
Abstract, PDF
[W1] M. Lange, M. Leucker, T. Noll, S. Tobies
Truth - a Verification Platform for Concurrent Systems
In Proceedings of Tools'98. Technical Report 9803, Christian-Albrechts University of Kiel, 1998.
Abstract


Unrefereed publications

[U8] M. Lange
Specifying Program Properties Using Modal Fixpoint Logics: A Survey of Results
In Proc. of the 8th Indian Conf. on Logic and its Applications, Delhi, IN, 2019
[U7] F. Bruse, O. Friedmann, M. Lange
Polynomial Guarded Transformation for the Modal μ-Calculus is Still Open
Highlights of Logics, Games and Automata, Paris, F, 2013
Abstract, PDF (arXiv long version with proof details)
[U6] M. Lange
Size-Change Termination and Satisfiability for Linear-Time Temporal Logics
In Proc. of the 8th International Symposium on Frontiers of Combining Systems, FroCoS'11, Saarbrücken, Germany, 2011,
volume 6989 of Lecture Notes in Computer Science, pages 28-39
Abstract, PDF (© Springer-Verlag)
[U5] M. Lange
The Complexity of the Emptiness and Word Problem for Visibly Pushdown Languages
In Proc. of the 20th Theorietag der GI-Fachgruppe Automaten und formale Sprachen, Baunatal, Germany, 2010,
Technical Report Kasseler Informatikschriften 3.
online version
[U4] M. Lange, M. Latte
A CTL-Based Logic for Program Abstractions
In Proc. of the 17th Int. Workshop on Logic, Language, Information and Computation, WoLLIC'10, Brasilia, BR, 2010
volume 6188 of Lecture Notes in Artificial Intelligence, pages 19-33
Abstract, PDF (© Springer-Verlag)
[U3] O. Friedmann, M. Lange
Tableaux with Automata
In Proceedings of the Workshop on Automata vs. Tableaux as Logical Decision Methods, AutoTab'09, Oslo, Norway, 2009
PDF
[U2] M. Lange
Temporal Logics for Non-Regular Properties: Model Checking
In Proceedings of the 4th Workshop Methods for Modalities, M4M-4, Berlin, Germany, 2005
volume 194 of Informatik Berichte, HU Berlin, pages 1-7
Abstract, PDF
[U1] M. Lange
Verification of Non-Regular Properties
In Proceedings of the 13. Theorietag der GI-Fachgruppe Automaten und Formale Sprachen, Herrsching, Germany, 2003,
Technical Report TUM-IO322, Munich University of Technology.
Abstract, PDF


Submitted

[S1] M. Sälzer, E. Alsmann, M. Lange
The Computational Complexity of Formal Reasoning for Encoder-Only Transformers


Preprints and Notes

[N1] M. Lange
A Note on the Expression Complexity of Bounded Variable Fragments of the Modal μ-Calculus
PDF


Dissertations

[D3] M. Lange
Temporal Logics Beyond Regularity
Habilitation Thesis, University of Munich, 2007
Abstract, PDF
[D2] M. Lange
Games for Modal and Temporal Logics
PhD Thesis, University of Edinburgh, 2002
Abstract, PDF (1.2MB)
[D1] M. Lange
Spielbasiertes Model Checking für den alternierungsfreien μ-Kalkül
Diplomarbeit, Aachen University of Technology, 1999
PDF