Martin Lange's homepage</a> <script type="text/javascript"> function highlight(n) { n.style.backgroundColor="#5179F1"; } function lowlight(n) { n.style.backgroundColor="#DCDCDC"; } </script> <style type="text/css"> body { background-color:#FFFFCC; } a { text-decoration:none } #bereich { line-height:1.1em } </style> </head> <body style="margin-left:40px"> <table border="0" style="float:left"> <tr align="left"> <table width="800" border="1" frame="void" cellspacing="0" cellpadding="0"> <tr> <td style="height:15px; width:100px; background-color:#DCDCDC" align="center" onmouseover="highlight(this)" onmouseout="lowlight(this)"> <a href="index.html" style="text-decoration:none; color:black">Home</a> </td> <td style="height:15px; width:100px; background-color:#DCDCDC" align="center" onmouseover="highlight(this)" onmouseout="lowlight(this)"> <a href="projects.html" style="text-decoration:none; color:black">Projects</a> </td> <td style="height:15px; width:100px; background-color:#002288" align="center"> <font style="color:white">Publications</font> </td> <td style="height:15px; width:100px; background-color:#DCDCDC" align="center" onmouseover="highlight(this)" onmouseout="lowlight(this)"> <a href="activities.html" style="text-decoration:none; color:black">Activities</a> </td> <td style="height:15px; width:100px; background-color:#DCDCDC" align="center" onmouseover="highlight(this)" onmouseout="lowlight(this)"> <a href="teaching.html" style="text-decoration:none; color:black">Teaching</a> </td> <td style="height:15px; width:100px; background-color:#DCDCDC" align="center" onmouseover="highlight(this)" onmouseout="lowlight(this)"> <a href="students.html" style="text-decoration:none; color:black">Students</a> </td> </tr> </table> <table width="90%" border="1" cellspacing="0" cellpadding="10" style="margin-top:-2px"> <tr> <td colspan="7" border="1"> <div id="bereich"> <a href="#journals">Journal papers</a> <br> <a href="#bookcontrib">Book contributions</a> <br> <a href="#conferences">Conference papers</a> <br> <a href="#workshops">Workshop papers</a> <br> <a href="#unrefereed">Unrefereed publications</a> <br> <a href="#submitted">Submitted papers</a> <br> <a href="#preprints">Preprints and Notes</a> <br> <a href="#theses">Theses</a> <br><br><hr> <a name="journals"> <h3>Journal papers</h3> M. Lange, H. Leiß<br> <b>To CNF or not to CNF? An Efficient Yet Presentable Version of the CYK Algorithm</b><br> <i>Informatica Didactica</i> 8, 2009<br> <font size="-1"> <A HREF="papers/abstracts.htm#2nfcyk">Abstract</a>, </font> <br><br> M. Lange<br> <b>Model Checking for Hybrid Logic</b><br> <i>Journal of Logic, Language and Information</i> 18(4):465-491, special issue on Hybrid Logic, 2009<br> <font size="-1"> <a href="papers/abstracts.htm#mchylo">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=jolli-hylo08">BibTeX</a> </font> <br><br> A. Søgaard, M. Lange<br> <b>Polyadic Dynamic Logics for HPSG Parsing</b><br> <i>Journal of Logic, Language and Information</i> 18(2):159-198, 2009<br> <font size="-1"> <a href="papers/abstracts.htm#ppdlhpsg">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=sl-ppdl08">BibTeX</a> </font> <br><br> M. Lange<br> <b>A Purely Model-Theoretic Proof of the Exponential Succinctness Gap between CTL<sup>+</sup> and CTL</b><br> <i>Information Processing Letters</i> 108:308-312, 2008<br> <font size="-1"> <a href="papers/abstracts.htm#ctlplussuccinct">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=ipl-ctlplus08">BibTeX</a> </font> <br><br> K. Brünnler, M. Lange<br> <b>Cut-Free Sequent Systems for Temporal Logic</b><br> <i>Journal of Logic and Algebraic Programming</i> 76(2):216-225, 2008<br> <font size="-1"> <a href="papers/abstracts.htm#gentzenltl">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=bl-jalp08">BibTeX</a> </font> <br><br> R. Axelsson, M. Lange, R. Somla<br> <b>The Complexity of Model Checking Higher-Order Fixpoint Logic</b><br> <i>Logical Methods in Computer Science</i> 3(2:7):1-33, 2007<br> <font size="-1"> <a href="papers/abstracts.htm#mchfl2">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=als-mchfl07">BibTeX</a>, <a href="papers/download.php?file=lmcs07.pdf">PDF</a> </font> <br><br> O. Grumberg, M. Lange, M. Leucker, S. Shoham <br> <b>When Not Losing Is Better than Winning: Abstraction and Refinement for the Full μ-Calculus</b><br> <i>Information and Computation</i> 205(8):1130-1148, 2007<br> <font size="-1"> <A HREF="papers/abstracts.htm#absrefnonlosing">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=glls:infcomp:07">BibTeX</a> </font> <br><br> M. Lange<br> <b>Three Notes on the Complexity of Model Checking Fixpoint Logic with Chop</b><br> <i>RAIRO - Theoretical Informatics and Applications</i> 41:177-190, 2007<br> <font size="-1"> <A HREF="papers/abstracts.htm#threenotes">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange:3mcflc:06">BibTeX</a> </font> <br><br> M. Lange<br> <b>The Alternation Hierarchy in Fixpoint Logic with Chop Is Strict Too</b><br> <i>Information and Computation</i> 204(9):1346-1367, 2006<br> <font size="-1"> <A HREF="papers/abstracts.htm#flcstrict">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange:ah-flc:06">BibTeX</a> </font> <br><br> M. Lange, R. Somla<br> <b>Propositional Dynamic Logic of Context-Free Programs and Fixpoint Logic with Chop</b><br> <i>Information Processing Letters</i> 100(2):72-75, 2006.<br> <font size="-1"> <A HREF="papers/abstracts.htm#pdlcflflc">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=langesomla-ipl06">BibTeX</a> </font> <br><br> M. Lange, C. Lutz<br> <b>2-ExpTime Lower Bounds for Propositional Dynamic Logics with Intersection</b><br> <i>Journal of Symbolic Logic</i> 70(4):1072-1086, 2005.<br> <font size="-1"> <A HREF="papers/abstracts.htm#ipdl2exptime">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=langelutz-jsl05">BibTeX</a> </font> <br><br> M. Lange<br> <b>Model Checking Propositional Dynamic Logic with All Extras</b><br> <i>Journal of Applied Logic</i> 4(1):39-49, 2005.<br> <font size="-1"> <A HREF="papers/abstracts.htm#mcpdl">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange-mcpdl">BibTeX</a>, </font> <br><br> M. Lange<br> <b>A Quick Axiomatisation of LTL with Past</b><br> <i>Mathematical Logic Quarterly</i> 51(1):83-88, 2005<br> <font size="-1"> <A HREF="papers/abstracts.htm#ltlpast">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange-ltlp05">BibTeX</a>, </font> <br><br> M. Lange, C. Stirling<br> <b>Model Checking Games for Branching Time Logics</b><br> <i>Journal of Logic and Computation</i> 12(4):623-639, special issue on ICTL'00, 2002<br> <font size="-1"> <A HREF="papers/abstracts.htm#jlc2000">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=LS-JLC2002">BibTeX</a>,  <a href="papers/jlc2000.pdf">PDF</a> </font> <br><br><br> <a name="bookcontrib"> <h3>Book contributions</h3> S. Kreutzer, M. Lange<br> <b>Non-Regular Fixed-Point Logics and Games</b><br> In J. Flum, E. Grädel, T. Wilke (eds.), <i>Logic and Automata: History and Perspectives</i>, vol. 2 of <i>Texts in Logic and Games</i>, pages 433-466, Amsterdam University Press, 2007<br> <font size="-1"> <A HREF="papers/abstracts.htm#nonreggames">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=kreutzerlange07">BibTeX</a> </font> <br><br> M. Lange<br> <b>A Lower Complexity Bound for Propositional Dynamic Logic with Intersection</b><br> In <i>Advances in Modal Logic Volume 5</i>, pages 133-147, 2005, King`s College Publications<br> <font size="-1"> <A HREF="papers/abstracts.htm#pdlisectexpspace">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange-aiml04book">BibTeX</a> </font> <br><br> M. Lange, M. Leucker, T. Noll, S. Tobies<br> <b>Truth - a Verification Platform for Concurrent Systems</b><br> In <i>Tool Support for System Specification, Development, and Verification,</i> Advances in Computing Science. Springer-Verlag Wien New York, 1999.<br> <font size="-1"> <A HREF="papers/abstracts.htm#tools98">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=LLNT">BibTeX</a> </font> <br><br><br> <a name="conferences"> <h3>Conference papers</h3> O. Friedmann, M. Lange<br> <b>Solving Parity Games in Practice</b><br> In <i>Proc. of the 7th Int. Symp. on Automated Technology for Verification and Analysis, ATVA'09</i>, Macao, China, 2009<br> volume <a href="http://www.springerlink.com/content/105633/">5799</a> of <i>Lecture Notes in Computer Science</i>, pages 182-196, © Springer-Verlag<br> <font size="-1"> <A HREF="papers/abstracts.htm#practsolv">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=fl-atva09">BibTeX</a>, <a href="papers/download.php?file=atva09.pdf">PDF</a> </font> <br><br> A. Kara, V. Weber, M. Lange, T. Schwentick<br> <b>On the Hybrid Extension of CTL and CTL+</b><br> In <i>Proc. of the 34th Int. Symp. on Mathematical Foundations of Computer Science, MFCS'09</i>, Novy Smokovec, Slovakia, 2009<br> volume <a href="http://www.springerlink.com/content/105633/">5734</a> of <i>Lecture Notes in Computer Science</i>, pages 427-438, © Springer-Verlag<br> <font size="-1"> <A HREF="papers/abstracts.htm#hybridctlplus">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=kwls-mfcs09">BibTeX</a>, </font> <br><br> C. Dax, F. Klaedtke, M. Lange<br> <b>On Regular Temporal Logics with Past Operators</b><br> In <i>Proc. of the 36th Int. Coll. on Automata, Languages and Programming, ICALP'09</i>, Rhodes Island, Greece, 2009<br> volume <a href="http://www.springerlink.com/content/105633/">5556</a> of <i>Lecture Notes in Computer Science</i>, pages 175-187, © Springer-Verlag<br> <font size="-1"> <A HREF="papers/abstracts.htm#pastpsl">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=dkl-icalp09">BibTeX</a>, <a href="papers/download.php?file=icalp09.pdf">PDF</a> </font> <br><br> R. Axelsson, K. Heljanko, M. Lange<br> <b>Analyzing Context-Free Grammars Using an Incremental SAT Solver</b><br> In <i>Proc. of the 35th Int. Coll. on Automata, Languages and Programming, ICALP'08</i>, Reykjavik, Iceland, 2008<br> volume <a href="http://www.springerlink.com/content/105633/">5126</a> of <i>Lecture Notes in Computer Science</i>, pages 410-422, © Springer-Verlag<br> <font size="-1"> <a href="papers/abstracts.htm#cfganalyzer">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=ahl-icalp08">BibTeX</a>, <a href="papers/download.php?file=icalp08.pdf">PDF</a> </font> <br><br> R. Axelsson, M. Lange<br> <b>Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic</b><br> In <i>Proc. of the 14th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'07</i>, Yerevan, Armenia, 2007,<br> volume <a href="http://www.springerlink.com/content/105633/">4790</a> of <i>Lecture Notes in Computer Science</i>, pages 62-76, © Springer-Verlag<br> <font size="-1"> <a href="papers/abstracts.htm#mchfl1">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=al-lpar07">BibTeX</a>, <a href="papers/download.php?file=lpar07.pdf">PDF</a> </font> <br><br> M. Lange<br> <b>Linear Time Logics around PSL: Complexity, Expressiveness, and a little bit of Succinctness</b><br> In <i>Proc. of the 18th Int. Conf. on Concurrency Theory, CONCUR'07</i>, Lisbon, Portugal, 2007<br> volume <a href="http://www.springerlink.com/content/105633/">4703</a> of <i>Lecture Notes in Computer Science</i>, pages 90-104, © Springer-Verlag<br> <font size="-1"> <a href="papers/abstracts.htm#pslcomplexity">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange-concur07">BibTeX</a>, <a href="papers/download.php?file=concur07.pdf">PDF</a> </font> <br><br> C. Dax, M. Hofmann, M. Lange<br> <b>A Proof System for the Linear Time μ-Calculus</b><br> In <i>Proc. of the 26th Conf. on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'06</i>, Kolkata, India, 2006<br> volume <a href="http://www.springerlink.com/content/105633/">4337</a> of <i>Lecture Notes in Computer Science</i>, pages 274-285, © Springer-Verlag <br> <font size="-1"> <A HREF="papers/abstracts.htm#mutlproof">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=dhl-fsttcs06">BibTeX</a>, <a href="papers/download.php?file=fsttcs06.pdf">PDF</a> </font> <br><br> K. Heljanko, T. Junttila, M. Keinänen, M. Lange, T. Latvala<br> <b>Bounded Model Checking for Weak Alternating Büchi Automata</b><br> In <i>Proceedings of the 18th Int. Conf. on Computer Aided Verification, CAV'06</i>, Seattle, WA, USA, 2006<br> volume <a href="http://www.springerlink.com/content/105633/">4144</a> of <i>Lecture Notes in Computer Science</i>, pages 95-108, © Springer-Verlag <br> <font size="-1"> <A HREF="papers/abstracts.htm#wababmc">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=hjkll-cav06">BibTeX</a>, <a href="papers/download.php?file=cav06.pdf">PDF</a> </font> <br><br> M. Lange, R. Somla<br> <b>The Complexity of Model Checking Higher Order Fixpoint Logic</b><br> In <i>Proc. of 30th Int. Symp. on Mathematical Foundations of Computer Science, MFCS'05</i>, Gdansk, Poland, 2005<br> volume <a href="http://www.springerlink.com/content/105633/" target="_top">3618</a> of <i>Lecture Notes in Computer Science</i>, pages 640-651, © Springer-Verlag <br> <font size="-1"> <A HREF="papers/abstracts.htm#mchfl">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=langesomla-mfcs05">BibTeX</a>, <a href="papers/download.php?file=mfcs05.pdf">PDF</a> </font> <br><br> M. Lange<br> <b>Weak Automata for the Linear Time μ-Calculus</b><br> In <i>Proceedings of the 6th Int. Conference on Verification, Model Checking and Abstract Interpretation, VMCAI'05</i>, Paris, France, 2005<br> volume <a href="http://www.springerlink.com/content/105633/" target="_top">3385</a> of <i>Lecture Notes in Computer Science</i>, pages 267-281, © Springer-Verlag <br> <font size="-1"> <A HREF="papers/abstracts.htm#mutlwapa">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange-wamutl05">BibTeX</a>, <a href="papers/download.php?file=vmcai05.pdf">PDF</a> </font> <br><br> O. Grumberg, M. Lange, M. Leucker, S. Shoham<br> <b>Don't Know in the μ-Calculus</b><br> In <i>Proceedings of the 6th Int. Conference on Verification, Model Checking and Abstract Interpretation, VMCAI'05</i>, Paris, France, 2005<br> volume <a href="http://www.springerlink.com/content/105633/" target="_top">3385</a> of <i>Lecture Notes in Computer Science</i>, pages 233-249, © Springer-Verlag <br> <font size="-1"> <A HREF="papers/abstracts.htm#threevaluedmucalc">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=GLLS:3valued05">BibTeX</a>, <a href="papers/download.php?file=vmcai05b.pdf">PDF</a> </font> <br><br> M. Lange<br> <b>A Lower Complexity Bound for Propositional Dynamic Logic with Intersection</b><br> In <i>Proceedings of Advances in Modal Logic 2004, AiML'04</i>, Manchester, UK, 2004<br> University of Manchester Technical Report UMCS-04-09-01<br> <font size="-1"> <A HREF="papers/abstracts.htm#pdlisectexpspace">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange-aiml04">BibTeX</a>, <a href="papers/download.php?file=aiml04.pdf">PDF</a> </font> <br><br> M. Lange<br> <b>Symbolic Model Checking of Non-Regular Properties</b><br> In <i>Proceedings of the 16th Int. Conf. on Computer Aided Verification, CAV'04</i>, Boston, MA, USA, 2004<br> volume <a href="http://www.springerlink.com/content/105633/" target="_top">3114</a> of <i>Lecture Notes in Computer Science</i>, pages 83-95, © Springer-Verlag <br> <font size="-1"> <A HREF="papers/abstracts.htm#flcbdd">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange-cav04">BibTeX</a>, <A HREF="papers/abstracts.htm#flcbdd">Disclaimer</a> </font> <br><br> M. Lange<br> <b>Satisfiability and Completeness of Converse-PDL Replayed</b><br> In <i>Proceedings of the 26th German Conference on Artificial Intelligence, KI'03</i>, Hamburg, Germany, 2003<br> volume <a href="http://www.springerlink.com/content/105633/" target="_top">2821</a> of <i>Lecture Notes in Artificial Intelligence</i>, pages 79-92, © Springer-Verlag<br> <font size="-1"> <A HREF="papers/abstracts.htm#conversepdl">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange-ki03">BibTeX</a>, <a href="papers/download.php?file=ki2003.pdf">PDF</a> </font> <br><br> J. Johannsen, M. Lange<br> <b>CTL+ is Complete for Double Exponential Time</b><br> In <i>Proceedings of the 30th Int. Colloquium on Automata, Languages and Programming, ICALP'03</i>, Eindhoven, The Netherlands, 2003<br> volume <a href="http://www.springerlink.com/content/105633/" target="_top">2719</a> of <i>Lecture Notes in Computer Science</i>, pages 767-775, © Springer-Verlag<br> <font size="-1"> <A HREF="papers/abstracts.htm#ctlplus-2exptime">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=JL-icalp03">BibTeX</a>, <a href="papers/download.php?file=icalp03.pdf">PDF</a> </font> <br><br> M. Lange<br> <b>Local Model Checking Games for Fixed Point Logic with Chop</b><br> In <i>Proceedings of the 13th International Conference on Concurrency Theory, CONCUR'02</i>, Brno, Czech Republic, 2002<br> volume <a href="http://www.springerlink.com/content/105633/" target="_top">2421</a> of <i>Lecture Notes in Computer Science</i>, pages 240-254, © Springer-Verlag<br> <font size="-1"> <A HREF="papers/abstracts.htm#flc-local">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange-concur02">BibTeX</a>, <a href="papers/download.php?file=concur02.pdf">PDF</a> </font> <br><br> M. Lange, C. Stirling<br> <b>Model Checking Fixed Point Logic with Chop</b><br> In <i>Proceedings of Foundations of Software Science and Computation Structures, FOSSACS'02</i>, Grenoble, France, 2002<br> volume <a href="http://www.springerlink.com/content/105633/" target="_top">2303</a> of <i>Lecture Notes in Computer Science</i>, pages 250-263, © Springer-Verlag<br> <font size="-1"> <A HREF="papers/abstracts.htm#mc-flc">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=ls-fossacs02">BibTeX</a>, <a href="papers/download.php?file=fossacs02.pdf">PDF</a> </font> <br><br> M. Lange, C. Stirling<br> <b>Focus Games for Satisfiability and Completeness of Temporal Logic</b><br> In <i>Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, LICS'01</i>, Boston, MA, USA, 2001<br> <font size="-1"> <A HREF="papers/abstracts.htm#lics2001">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lics2001">BibTeX</a>, <a href="papers/download.php?file=lics2001.pdf">PDF</a> </font> <br><br> M. Lange, C. Stirling<br> <b>Model Checking Games for CTL*</b><br> In <i>Proceedings of the International Conference on Temporal Logic, ICTL'2000</i>, Leipzig, Germany, 2000<br> <font size="-1"> <A HREF="papers/abstracts.htm#ictl2000">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=ictl2000">BibTeX</a>, <a href="papers/download.php?file=ictl2000.pdf">PDF</a> </font> <br><br><br> <a name="workshops"> <h3>Workshop papers</h3> O. Friedmann, M. Lange<br> <b>A Solver for Modal Fixpoint Logics</b><br> To appear in <i>Proc. of the 6th Workshop on Methods for Modalities, M4M-6</i>, Copenhagen, Denmark, 2009<br> <font size="-1"> <A HREF="papers/abstracts.htm#mlsolver">Abstract</a>, </font> <br><br> S. Kreutzer, M. Lange<br> <b>A Note on the Relation between Inflationary Fixpoints and Least Fixpoints of Higher-Order</b><br> In <i>Proc. of the 6th Workshop on Fixed Points in Computer Science, FICS'09</i>, Coimbra, Portugal, 2009<br> <font size="-1"> <A HREF="papers/abstracts.htm#ifplfpho">Abstract</a>, </font> <br><br> M. Lange<br> <b>Solving Parity Games by a Reduction to SAT</b><br> In <i>Proc. of the Workshop on Games in Design and Verification, GDV'05</i>, Edinburgh, Scotland, UK, 2005<br> <font size="-1"> <A HREF="papers/abstracts.htm#paritysat">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange-gdv05">BibTeX</a>, <a href="papers/download.php?file=gdv05.pdf">PDF</a> </font> <br><br> M. Jehle, J. Johannsen, M. Lange, N. Rachinsky<br> <b>Bounded Model Checking for All Regular Properties</b><br> In <i>Proc. of the 3rd Int. Workshop on Bounded Model Checking, BMC'05</i>, Edinburgh, Scotland, UK, 2005<br> volume 144.1 of <i>Elect. Notes in Theor. Comp. Science</i>, pages 3-18, Elsevier Science, 2005<br> <font size="-1"> <A HREF="papers/abstracts.htm#bmcmulin">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=jjlr-bmc05">BibTeX</a>, <a href="papers/download.php?file=bmc05.pdf">PDF</a> </font> <br><br> M. Lange, H. W. Loidl<br> <b>Parallel and Symbolic Model Checking for Fixpoint Logic with Chop</b><br> In <i>Proc. of the 3rd Int. Workshop on Parallel and Distributed Methods in Verification, PDMC'04</i>, London, UK,<br> volume 128.3 of <i>Elect. Notes in Theor. Comp. Science</i>, pages 125-138, Elsevier Science, 2005<br> <font size="-1"> <A HREF="papers/abstracts.htm#parsymbflc">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=ll-pdmc04">BibTeX</a>, <a href="papers/download.php?file=pdmc04.pdf">PDF</a> </font> <br><br> C. Dax, M. Lange<br> <b>Game Over: The Foci Approach to LTL Satisfiability and Model Checking</b><br> In <i>Proc. of the Workshop on Games in Design and Verification, GDV'04</i>, Boston, MA, USA, <br> volume 119.1 of <i>Elect. Notes in Theor. Comp. Science</i>, pages 33-49, Elsevier Science, 2005<br> <font size="-1"> <A HREF="papers/abstracts.htm#focigames">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=dl-gdv04">BibTeX</a>, <a href="papers/download.php?file=gdv04.pdf">PDF</a> </font> <br><br> M. Lange<br> <b>Alternating Context-Free Languages and Linear Time μ-Calculus with Sequential Composition</b><br> In <i>Proceedings of the 9th Int. Workshop on Expressiveness in Concurrency, EXPRESS'02</i>, Brno, Czech Republic, 2002<br> volume 68.2 of <i>Electr. Notes in Theor. Comp. Science</i>, Elsevier Science<br> <font size="-1"> <A HREF="papers/abstracts.htm#acfllflc">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange-express02">BibTeX</a>, <a href="papers/download.php?file=express02.pdf">PDF</a> </font> <br><br> M. Lange<br> <b>A Game Based Approach to CTL* Model Checking</b><br> In <i>Proceedings of the summer school MOVEP'2k</i>, Nantes, France, 2000<br> <font size="-1"> <A HREF="papers/abstracts.htm#movep2k">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=movep2k">BibTeX</a>, <a href="papers/download.php?file=movep2k.pdf">PDF</a> </font> <br><br> M. Lange, M. Leucker, T. Noll, S. Tobies<br> <b>Truth - a Verification Platform for Concurrent Systems</b><br> In <i>Proceedings of Tools'98</i>. Technical Report 9803, Christian-Albrechts University of Kiel, 1998. <br> <font size="-1"> <A HREF="papers/abstracts.htm#tools98">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=LLNT">BibTeX</a>  </font> <br><br><br> <a name="unrefereed"> <h3>Unrefereed publications</h3> M. Lange<br> <b>Temporal Logics for Non-Regular Properties: Model Checking</b><br> In <i>Proceedings of the 4th Workshop Methods for Modalities, M4M-4</i>, Berlin, Germany, 2005<br> volume 194 of Informatik Berichte, HU Berlin, pages 1-7<br> <font size="-1"> <A HREF="papers/abstracts.htm#m4mnonreg">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=lange-m4m">BibTeX</a>, <a href="papers/download.php?file=m4mnonreg.pdf">PDF</a> </font> <br><br> M. Lange<br> <b>Verification of Non-Regular Properties</b><br> In <i>Proceedings of the 13. Theorietag der GI-Fachgruppe Automaten und Formale Sprachen</i>, Herrsching, Germany, 2003,<br> Technical Report TUM-IO322, Munich University of Technology.<br> <font size="-1"> <A HREF="papers/abstracts.htm#gi03forspra">Abstract</a>, <a href="http://www.tcs.ifi.lmu.de/cgi-bin/lookbibtex.cgi?pattern=gi03forspra">BibTeX</a>, <a href="papers/download.php?file=gi03fospra.pdf">PDF</a> </font> <br><br><br> <a name="submitted"> <h3>Submitted</h3>  C. Dax, F. Klaedtke, M. Lange<br> <b>On Regular Temporal Logics with Past</b><br> <font size="-1"> <A HREF="papers/abstracts.htm#pastpsl2">Abstract</a> </font> <br><br> K. Heljanko, M. Keinänen, M. Lange, I. Niemelä<br> <b>Solving Parity Games by a Reduction to SAT</b><br> <font size="-1"> <A HREF="papers/abstracts.htm#parity2diff">Abstract</a> </font> <br><br> O. Friedmann, M. Lange, M. Latte<br> <b>An Effective System of Infinite Proofs for the Full Computation Tree Logic</b><br> <font size="-1"> <A HREF="papers/abstracts.htm#ctlstarinfsystem">Abstract</a>, </font> <br><br>  <br> <a name="preprints"> <h3>Preprints and Notes</h3> M. Lange<br> <b>A Note on the Expression Complexity of Bounded Variable Fragments of the Modal μ-Calculus</b><br> <font size="-1"> <a href="papers/bvarexprcompmucalc.pdf">PDF</a> </font> <br><br> <a name="theses"> <h3>Theses</h3> M. Lange<br> <b>Temporal Logics Beyond Regularity</b><br> Habilitation Thesis, University of Munich, 2007<br> <font size="-1"> <A HREF="papers/abstracts.htm#habil">Abstract</a>, <a href="papers/download.php?file=habil.pdf">PDF</a> </font> <br><br> M. Lange<br> <b>Games for Modal and Temporal Logics</b><br> PhD Thesis, University of Edinburgh, 2002<br> <font size="-1"> <A HREF="papers/abstracts.htm#dissertation">Abstract</a>, <a href="papers/download.php?file=thesis.pdf">PDF</a> (1.2MB) </font> <br><br> M. Lange<br> <b>Spielbasiertes Model Checking für den alternierungsfreien μ-Kalkül</b><br> Diplomarbeit, Aachen University of Technology, 1999 <br> <font size="-1"> <a href="papers/download.php?file=diplomarbeit.pdf">PDF</a> </font> <br><br><br> </div> </td> </tr> </table> </tr> </table> </body>