



Universität Leipzig Institut für Informatik Automaten und Sprachen Karin Quaas 
Karin Quaas 

Refereed Conference Papers 





2017 

Revisiting Reachability in Timed Automata (with M. Shirmohammadi and J. Worrell). In ThirtySecond Annual ACM/IEEE Symposium on
Logic in Computer Science (LICS 2017), accepted. 


The Complexity of Flat Freeze LTL (with B. Bollig and A. Sangnier). In 28th Int. Conference on Concurrency Theory (CONCUR 2017), accepted. 


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), accepted. 


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), 326339, LNCS 9168. 


2014 

Verification for Timed Automata Extended with Unbounded Discrete Data
Structures. In 25th Int. Conference on Concurrency Theory (CONCUR 2014), 512526, LNCS 8704. 


On the Expressiveness of TPTL and MTL over omegaData Words (with C. Carapelle, O. Fernandez Gil, S. Feng). In 14th Int. Conference Automata and Formal Languages (AFL 2014), 518, EPTCS 145. 


MTLModel Checking of OneClock Parametric Timed Automata is Undecidable. In 1st Int. Workshop on Synthesis of Continuous Parameters (SynCoP 2014), 518, EPTCS 145. 


Satisfiability for MTL and TPTL over Nonmonotonic Data Words (with C. Carapelle, S. Feng, O. Fernandez Gil). In Language and Automata Theory and Applications (LATA 2014), 248259, 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), 102117, Springer LNCS, Volume 8172. 


Model Checking Metric Temporal Logic over Automata with one Counter. In Language and Automata Theory and Applications (LATA 2013), 468479, Springer LNCS, Volume 7810. 


2011 

On the IntervalBound Problem for Weighted Timed Automata. In Language and Automata Theory and Applications (LATA 2011), 452464, Springer LNCS, Volume 6638. 


2009 

On the Supports of Recognizable Timed Series. In Formal Modeling and Analysis of Timed Systems (FORMATS 2009), 243257, Springer LNCS, Volume 5813.



Weighted Timed MSO Logics. In Developments in Language Theory (DLT 2009), 419430, Springer LNCS, Volume 5583.



2008 

A KleeneSchützenberger Theorem for Weighted Timed Automata (with M. Droste). In Foundations of Software Science and Computational Structures (FoSSaCS 2008), 142156, Springer LNCS, Volume 4962. 


2007 

ZoneBased Universality Analysis for SingleClock Timed Automata (with P. A. Abdulla, J. Ouaknine and J. Worrell). In International Symposium on Fundamentals of Software Engineering 2007, 98112, Springer LNCS, Volume 4767. 
Fully Refereed Papers 





2017 

Path Checking for MTL and TPTL over Data Words (with S. Feng and M. Lohrey). In Logical Methods in Computer Science, accepted. 


2015 

Verification for timed automata extended with unbounded discrete data structures. In Logical Methods in Computer Science11(3), 2015. 


2014 

Parameterized Model Checking of Weighted Networks (with I. Meinecke). In Theoretical Computer Science, 534: 6985, 2014. 


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):500502, 2011. 


MSO Logics for Weighted Timed Automata. In Formal Methods in System Design, 38(3):193222, 2011. 


A KleeneSchützenberger Theorem for Weighted Timed Automata (with M. Droste). In Theoret. Comp. Science 412: 11401153, 2011. 


2008 

A Universality Analysis for OneClock Timed Automata (with P. A. Abdulla, J. Deneux, J. Ouaknine and J. Worrell). In Fundamenta Informaticae 89(4):419450, 2008. 


PhD Thesis 





KleeneSchützenberger and Büchi Theorems for Weighted Timed Automata. 