Home Projects Publications Activities Teaching Students
Text books
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


Journal papers

[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

[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

[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. ?? of LIPIcs, pages ??-??
Abstract
[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. ?? of Lecture Notes in Computer Science, pages ??-??, Springer
Abstract
[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. ?? of Lecture Notes in Computer Science, pages ??-??, Springer
Abstract
[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
[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,
[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 Proceedings 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 Proceedings 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 Proceedings 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 Proceedings 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 Proceedings 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 Proceedings 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 Proceedings 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 Proceedings 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 Proceedings 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 Proceedings 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 Proceedings of the International Conference on Temporal Logic, ICTL'2000, Leipzig, Germany, 2000
Abstract, PDF


Workshop papers

[W14] A. Ehle, N. Hundeshagen, M. Lange
Automated Reasoning in the Sequent Calculus Trainer
In Proc. of the Workshop on Theorem Proving Components for Educational Software, Gothenburg, S, 2017
Abstract
[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

[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



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