Publications

The content on this page was translated automatically.

2023

Alexander Artikis, Florian Bruse, Luke Hunsberger
30th International Symposium on Temporal Representation and Reasoning
TIME 2023, September 25-26, 2023, NCSR Demokritos, Athens, Greece.LIPIcs 278, Schloss Dagstuhl - Leibniz Center for Informatics 2023, ISBN 978-3-95977-298-3

 M. Sälzer, Beddar-Wiesing
Time-Aware Robustness of Temporal Graph Neural Networks for Link Prediction (Extended Abstract)
TIME 2023
 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
 M. Sälzer, M. Lange
Reachability in Simple Neural Networks
Fundamenta Informaticae, 189(3-4):241-259, special issue on RP'21, 2023
 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
 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
 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
 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
 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
2022F. 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
 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
 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
 M. Herwig, N. Hundeshagen, M. Lange
Towards Graphical Feedback in the DiMo Learning Tool
Formal Methods Education Online: Tips, Tricks & Tools, FOMEO'22, Haifa, IL, 2022
 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
2021M. 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
 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
 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
 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
 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
 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
 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
 M. Sälzer, G. Siebert
Towards Learning From Graph Representable Formal Models
OVERLAY@GandALF 2021
 F. Bruse, M. Lange
Temporal logic with recursion
Information and Computation 281 (2021)
 F. Bruse, M. Lange, E. Lozes
The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic
Fundamenta Informaticae 178(1-2) (2021)
2020

D. Kernberger, M. Lange
On the Expressive Power of Hybrid Branching-Time Logics
Theoretical Computer Science 813:362-374, 2020

 

D. Kernberger, M. Lange
Model Checking for Hybrid Branching-Time Logics
Journal of Logic and Algebraic Programming 110, special issue on TIME'16, 2020

 

M. Kastaun, M. Meier, N. Hundeshagen, M. Lange
ProfiLL: Professionalization through intelligent teaching-learning systems
In Bildung, Schule, Digitalisierung, Waxmann-Verlag, 2020

 

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

 

F. Bruse, M. Lange
Temporal Logic with Recursion
In Proc. of the 27th Int. Symp. on Temporal Representation and Reasoning, TIME'20, Bolzano, IT, 2020
vol. 178 of  LIPIcs, pages 6:1-6:14

 

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

 

F. Bruse
Extremal Fixpoints for Higher-Order Modal Logic. Kassel, Germany 2018
Dissertation 2020

2019Martin Lange
Specifying Program Properties Using Modal Fixpoint Logics: A Survey of Results
ICLA 2019: 42-51
 Christoph Eickhoff, Martin Lange, Simon-Lennert Raesch, Albert Zündorf
EMFeR: Model Checking for Object Oriented (EMF) Models
MODELSWARD 2019: 511-518
 Klaus David, Kurt Geihs, Martin Lange, Gerd Stumme
INFORMATIK 2019: 50 Jahre Gesellschaft für Informatik - Informatik für Gesellschaft, 23-26.9.2019, Kassel, Germany
LNI P-294, GI 2019, ISBN 978-3-88579-688-6
 Claude Draude, Martin Lange, Bernhard Sick
INFORMATIK 2019: 50 Jahre Gesellschaft für Informatik - Informatik für Gesellschaft (workshop contributions), 23-26.9.2019, Kassel, Germany
LNI P-295, GI 2019, ISBN 978-3-88579-689-3
2018D. Kernberger, M. Lange
Model Checking for Hybrid Branching-Time Logics
To appear in Journal of Logic and Algebraic Programming, special issue on TIME'16, 2018
 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
 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
 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
2017D. 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
 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
 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
 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
 M. Hutagalung
Topological Characterization of Multi-Buffer Simulation
In Proc. of the Reachability Problem - 11th International Workshop, London, UK, 2017, vol. 10506 of Lecture Notes in Computer Science, pp. 101-117
2016S. 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
2015O. 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
2014M. 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 Relativization
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
2013O. 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
2012E. 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
2011B. 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 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
2010R. 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