Search

• < Previous
• 1
• Next >

---

On the Expressive Power of 2-Stack Visibly Pushdown Automata

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,&nbsp;[&hellip;]

---

Propositional Dynamic Logic for Message-Passing Systems

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&nbsp;[&hellip;]

---

The Complexity of Flat Freeze LTL

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&nbsp;[&hellip;]

---

Bounded Reachability Problems are Decidable in FIFO Machines

Benedikt Bollig ; Alain Finkel ; Amrita Suresh.

The undecidability of basic decision problems for general FIFO machines such as reachability and unboundedness is well-known. In this paper, we provide an underapproximation for the general model by considering only runs that are input-bounded (i.e. the sequence of messages sent through a particular&nbsp;[&hellip;]

---

Analyzing Robustness of Angluin's L$^*$ Algorithm in Presence of Noise

Lina Ye ; Igor Khmelnitsky ; Serge Haddad ; Benoît Barbot ; Benedikt Bollig ; Martin Leucker ; Daniel Neider ; Rajarshi Roy.

Angluin's L$^*$ algorithm learns the minimal deterministic finite automaton (DFA) of a regular language using membership and equivalence queries. Its probabilistic approximatively correct (PAC) version substitutes an equivalence query by numerous random membership queries to get a high level&nbsp;[&hellip;]

---

Branch-Well-Structured Transition Systems and Extensions

Benedikt Bollig ; Alain Finkel ; Amrita Suresh.

We propose a relaxation to the definition of well-structured transition systems (\WSTS) while retaining the decidability of boundedness and non-termination. In this class, the well-quasi-ordered (wqo) condition is relaxed such that it is applicable only between states that are reachable one from&nbsp;[&hellip;]

---

On the Satisfiability of Local First-Order Logics with Data

Benedikt Bollig ; Arnaud Sangnier ; Olivier Stietel.

We study first-order logic over unordered structures whose elements carry a finite number of data values from an infinite domain. Data values can be compared wrt.\ equality. As the satisfiability problem for this logic is undecidable in general, we introduce a family of local fragments. They&nbsp;[&hellip;]

---