3 results
Benedikt Bollig ; Karin Quaas ; Arnaud Sangnier.
We consider the model-checking problem for freeze LTL on one-counter automata (OCA). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable […]
Published on September 30, 2019
Benedikt Bollig ; Dietrich Kuske ; Ingmar Meinecke.
We examine a bidirectional propositional dynamic logic (PDL) for finite and infinite message sequence charts (MSCs) extending LTL and TLC-. By this kind of multi-modal logic we can express properties both in the entire future and in the past of an event. Path expressions strengthen the classical […]
Published on September 4, 2010
Benedikt Bollig.
Visibly pushdown automata are input-driven pushdown automata that recognize some non-regular context-free languages while preserving the nice closure and decidability properties of finite automata. Visibly pushdown automata with multiple stacks have been considered recently by La Torre, Madhusudan, […]
Published on December 24, 2008