Universität Leipzig    Institut für Informatik    Automaten und Sprachen    Karin Quaas
Karin Quaas
  2017
Path Checking for MTL and TPTL (with S. Feng and M. Lohrey). In Logical Methods in Comp. Science, 13(3).
Revisiting Reachability in Timed Automata (with M. Shirmohammadi and J. Worrell). In Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), 1-12.
The Complexity of Flat Freeze LTL (with B. Bollig and A. Sangnier). In 28th Int. Conference on Concurrency Theory (CONCUR 2017), 33:1-33:16.
An Algebraic Approach to Energy Problems I (with Z. Esik, U. Fahrenberg and A. Legay). In Acta Cybern., 23(1): 203-228.
An Algebraic Approach to Energy Problems II (with Z. Esik, U. Fahrenberg and A. Legay). In Acta Cybern., 23(1): 229-268.
  2016
Synchronizing Data Words for Register Automata (with P. Babari and M. Shirmohammadi). In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016), 15:1-15:15.
  2015
Verification for timed automata extended with unbounded discrete data structures. In Logical Methods in Computer Science 11(3), 2015.
Path Checking for MTL and TPTL over Data Words (with S. Feng and M. Lohrey). In 19th Int. Conference Developments in Language Theory (DLT 2015), 326-339, LNCS 9168.
  2014
Parameterized Model Checking of Weighted Networks (with I. Meinecke). In Theoretical Computer Science, 534: 69-85, 2014.
Verification for Timed Automata Extended with Unbounded Discrete Data Structures. In 25th Int. Conference on Concurrency Theory (CONCUR 2014), 512-526, LNCS 8704.
On the Expressiveness of TPTL and MTL over omega-Data Words (with C. Carapelle, O. Fernandez Gil, S. Feng). In 14th Int. Conference Automata and Formal Languages (AFL 2014), 5-18, EPTCS 145.
MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable. In 1st Int. Workshop on Synthesis of Continuous Parameters (SynCoP 2014), 5-18, EPTCS 145.
Satisfiability for MTL and TPTL over Non-monotonic Data Words (with C. Carapelle, S. Feng, O. Fernandez Gil). In Language and Automata Theory and Applications (LATA 2014), 248-259, Springer LNCS, Volume 8370.
  2013
Kleene Algebras and Semimodules for Energy Problems (with U. Fahrenberg, A. Legay, Z. Ésik). In 11th International Symposium on Automated Technology for Verification and Analysis (ATVA 2013), 102-117, Springer LNCS, Volume 8172.
Model Checking Metric Temporal Logic over Automata with one Counter. In Language and Automata Theory and Applications (LATA 2013), 468-479, Springer LNCS, Volume 7810.
  2011
Recognizability of the Support of Recognizable Series over the Semiring of the Integers is Undecidable (with D. Kirsten). In Information Processing Letters, 111(10):500-502, 2011.
MSO Logics for Weighted Timed Automata. In Formal Methods in System Design, 38(3):193-222, 2011.
A Kleene-Schützenberger Theorem for Weighted Timed Automata (with M. Droste). In Theoret. Comp. Science 412: 1140-1153, 2011.
On the Interval-Bound Problem for Weighted Timed Automata. In Language and Automata Theory and Applications (LATA 2011), 452-464, Springer LNCS, Volume 6638.
  2009
On the Supports of Recognizable Timed Series. In Formal Modeling and Analysis of Timed Systems (FORMATS 2009), 243-257, Springer LNCS, Volume 5813.
Weighted Timed MSO Logics. In Developments in Language Theory (DLT 2009), 419-430, Springer LNCS, Volume 5583.
  2008
A Universality Analysis for One-Clock Timed Automata (with P. A. Abdulla, J. Deneux, J. Ouaknine and J. Worrell). In Fundamenta Informaticae 89(4):419-450, 2008.
A Kleene-Schützenberger Theorem for Weighted Timed Automata (with M. Droste). In Foundations of Software Science and Computational Structures (FoSSaCS 2008), 142-156, Springer LNCS, Volume 4962.
  2007
Zone-Based Universality Analysis for Single-Clock Timed Automata (with P. A. Abdulla, J. Ouaknine and J. Worrell). In International Symposium on Fundamentals of Software Engineering 2007, 98-112, Springer LNCS, Volume 4767.