Publications

2016 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
  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
  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, pp. 120-134
  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, pp. 213-227
  M. Hutagalung, N. Hundeshagen, D. Kuske, M. Lange, E. Lozes
Two-Buffer Simulation Games
In Proc. of the CASSTING'16 Workshop, Eindhoven, NL, 2016
vol. 220 of Electronic Proceedings in Theoretical Computer Science, pp. 27-38
2015 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
  F. Grandi, M. Lange, A. Lomuscio (eds.)
22nd International Symposium on Temporal Representation and Reasoning, TIME'15
Kassel, D, September 23-25, 2015
IEEE Computer Society
  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 LNCS, pp. 327-338, Springer
  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
  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
vol. 191 of Electronic Proceedings in Theoretical Computer Science, pp. 105-116
  M. Folschette, L. Pauleve, M. Magnin, O. Roux
Sufficient Conditions for Reachability in Automata Networks with Priorities
Theoretical Computer Science, special edition From Computer Science to Biology and Back 608(1): 66–83, 2015
  E. B. Abdallah, M. Folschette, O. Roux, M. Magnin
Exhaustive Analysis of Dynamical Properties of Biological Regulatory Networks with Answer Set Programming
In Proc. of the IEEE International Conference on Bioinformatics and Biomedicine, BIBM’15, Washington, USA, 2015
pp. 281–285, IEEE
2014 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 LNCS, pp. 90-103, Springer
  F. Bruse
Alternating Parity Krivine Automata
In Proc. of the 39th Int. Symp. on Mathematical Foundations of Computer Science, MFCS'14, Budapest, HU, 2014
vol. 8634 of LNCS, pp. 111-122
  N. Hundeshagen, P. Leupold
Transducing by observing length-reducing and painter rules
RAIRO - Theor. Inf. and Applic. 48(1): 85-105, 2014
  N. Hundeshagen, F. Otto
Restarting Transducers, Regular Languages, and Rational Relations
Theory of Computing Systems 1432-4350: 1-31, 2014
  R. Ehlers, U. Topcu
Resilience to Intermittent Assumption Violations in Reactive Synthesis
In Proc. of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC'14, Berlin, D, 2014
pp. 203-212, ACM
  R. Ehlers, S. A. Seshia, H. Kress-Gazit
Synthesis with Identifiers
15th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI'14
vol. 8318 of LNCS, pp. 415-433, Springer
  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, pp. 116-130, 2013
  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, pp. 286-300, 2014
  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
  F. Bruse, O. Friedmann, M. Lange
On Guarded Transformation in the Modal µ-Calculus
Logic Journal of the IGPL 23(2): 194-216, 2014
  M. Lange, E. Lozes, M. Vargas Guzman
Model Checking Process Equivalences
Theoretical Computer Science 560(3):326-347, special issue on GandALF'12, 2014
  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
  R. Ehlers, M. Lange
A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic
In Proc. of the 7th Int. Joint Conf. on Automated Reasoning, IJCAR'14, Vienna, A, 2014
vol. 8562 of LNCS, pp. 360-366, Springer
  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 LNCS, pp. 190-203, Springer
2013 O. Friedmann, M. Lange
Deciding the Unguarded Modal µ-Calculus
Journal of Applied Non-Classical Logics 23(4):353-371, 2013
  O. Friedmann, M. Latte, M. Lange
Satisfiability Games for Branching-Time Logics
Logical Methods in Computer Science 9(4:5), 2013
  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
vol. 7966 of LNCS, pp. 224-237, Springer, 2013
  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 LNCS, pp. 347-358, 2013, Springer
2012 E. Lozes, J. Villard
Reliable Contracts for Unreliable Half-Duplex Communications
revised selected papers of the 8th Int. Workshop on Web Services and Formal Methods, WS-FM'11
vol. 7176 of LNCS, pp. 2-16, Springer, 2012
  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 Electronic Proceedings in Theoretical Computer Science, pp. 113-126
  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 Electronic Proceedings in Theoretical Computer Science, pp. 43-56
  K. Heljanko, M. Keinänen, M. Lange, I. Niemelä
Solving Parity Games by a Reduction to SAT
Journal of Computer and System Sciences 78:430-440, special issue on Games in Verification, 2012
  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 LNCS, pp 393-407, 2012, Springer
  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 LNCS, pp. 64-78, 2012, Springer
  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
vol. 77 of Electronic Proceedings in Theoretical Computer Science, pp. 39-46
  F. Jacquemard, E. Lozes, R. Treinen, J. Villard
Multiple Congruence Relations, First-Order Theories on Terms, and the Frames of the Applied Pi-Calculus
revised selected papers of the workshop on Theory of Security and Applications, TOSCA'11
vol. 6993 of LNCS, pp. 166-185, Springer, 2012
2011 B. Badban, M. Lange
Exact Incremental Analysis of Timed Automata Using an SMT Solver
In Proc. of the 9th Int. Conf. on Formal Modelling and Analysis of Timed Systems, FORMATS'11, Aalborg, DK, 2011
vol. 6919 of LNCS, pp. 177-192, Springer
  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
vol. 6989 of LNCS, pp. 28-39, Springer
  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
vol. 6945 of LNCS, pp. 45-57, Springer
  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
vol. 6793 of LNCS, pp. 149-163, 2011, Springer
  M. Lange
P-Hardness of the Emptiness Problem for Visibly Pushdown Languages
Information Processing Letters 111(7):338-341, 2011
2010 R. Axelsson, M. Hague, S. Kreutzer, M. Lange, M. Latte
Extended Computation Tree Logic
In Proc. of the 17th Int. Conf. on Programming, Artificial Intelligence and Reasoning LPAR'10, Yogyakarta, RI, 2010
vol. 6397 of LNCS, pp. 67-81, Springer
  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
vol. 25 of Electronic Notes in Theoretical Computer Science, pp. 118-131, 2010
  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
vol. 6173 of Lecture Notes in Artificial Intelligence, pp. 331-345, Springer
  C. Dax, F. Klaedtke, M. Lange
On Regular Temporal Logics with Past
Acta Informatica 47(4):251-277, 2010
  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
vol. 6188 of Lecture Notes in Artificial Intelligence, pp. 19-33, Springer