Search

• < Previous
• 1
• Next >

---

Expressiveness of Metric modalities for continuous time

Yoram Hirshfeld ; Alexander Rabinovich.

We prove a conjecture by A. Pnueli and strengthen it showing a sequence of "counting modalities" none of which is expressible in the temporal logic generated by the previous modalities, over the real line, or over the positive reals. Moreover, there is no finite temporal logic that can express all&nbsp;[&hellip;]

---

The Church Problem for Countable Ordinals

Alexander Rabinovich.

A fundamental theorem of Buchi and Landweber shows that the Church synthesis problem is computable. Buchi and Landweber reduced the Church Problem to problems about &#969;-games and used the determinacy of such games as one of the main tools to show its computability. We consider a natural&nbsp;[&hellip;]

---

The complexity of linear-time temporal logic over the class of ordinals

Stephane Demri ; Alexander Rabinovich.

We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic by Kamp's theorem. We show that it has a PSPACE-complete satisfiability problem over the class of ordinals. Among the consequences of our&nbsp;[&hellip;]

---

The Church Synthesis Problem with Parameters

Alexander Rabinovich.

For a two-variable formula &psi;(X,Y) of Monadic Logic of Order (MLO) the Church Synthesis Problem concerns the existence and construction of an operator Y=F(X) such that &psi;(X,F(X)) is universally valid over Nat. B\"{u}chi and Landweber proved that the Church synthesis problem is decidable;&nbsp;[&hellip;]

---

Decidable Expansions of Labelled Linear Orderings

Alexis Bes ; Alexander Rabinovich.

Consider a linear ordering equipped with a finite sequence of monadic predicates. If the ordering contains an interval of order type \omega or -\omega, and the monadic second-order theory of the combined structure is decidable, there exists a non-trivial expansion by a further monadic predicate that&nbsp;[&hellip;]

---

A Proof of Kamp's theorem

Alexander Rabinovich.

We provide a simple proof of Kamp's theorem.

---

A Proof of Stavi's Theorem

Alexander Rabinovich.

Kamp's theorem established the expressive equivalence of the temporal logic with Until and Since and the First-Order Monadic Logic of Order (FOMLO) over the Dedekind-complete time flows. However, this temporal logic is not expressively complete for FOMLO over the rationals. Stavi introduced two&nbsp;[&hellip;]

---

Ambiguity Hierarchy of Regular Infinite Tree Languages

Alexander Rabinovich ; Doron Tiferet.

An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is k-ambiguous (for k > 0) if for every input it has at most k accepting computations. An automaton is boundedly ambiguous if it is k-ambiguous for some $k \in \mathbb{N}$. An automaton is finitely&nbsp;[&hellip;]

---