8 Search Results for "Rabinovich, Alexander"

Document
DOI: 10.4230/LIPIcs.TIME.2022.10
Gabbay Separation for the Duration Calculus

Authors: Dimitar P. Guelev

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)

Abstract
Gabbay’s separation theorem about linear temporal logic with past has proved to be one of the most useful theoretical results in temporal logic. In particular it enables a concise proof of Kamp’s seminal expressive completeness theorem for LTL. In 2000, Alexander Rabinovich established an expressive completeness result for a subset of the Duration Calculus (DC), a real-time interval temporal logic. DC is based on the chop binary modality, which restricts access to subintervals of the reference time interval, and is therefore regarded as introspective. The considered subset of DC is known as the ⌈P⌉-subset in the literature. Neighbourhood Logic (NL), a system closely related to {DC}, is based on the neighbourhood modalities, also written ⟨A⟩ and ⟨ ̄A⟩ in the notation stemming from Allen’s system of interval relations. These modalities are expanding as they allow writing future and past formulas to impose conditions outside the reference interval. This setting makes temporal separation relevant: is expressive power ultimately affected, if past constructs are not allowed in the scope of future ones, or vice versa? In this paper we establish an analogue of Gabbay’s separation theorem for the ⌈P⌉-subset of the extension of DC by the neighbourhood modalities, and the ⌈P⌉-subset of the extension of DC by the neighbourhood modalities and chop-based analogue of Kleene star. We show that the result applies if the weak chop inverses, a pair binary expanding modalities, are given the role of the neighbourhood modalities, by virtue of the inter-expressibility between them and the neighbourhood modalities in the presence of chop.
Cite as

Dimitar P. Guelev. Gabbay Separation for the Duration Calculus. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 10:1-10:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{guelev:LIPIcs.TIME.2022.10,
  author =	{Guelev, Dimitar P.},
  title =	{{Gabbay Separation for the Duration Calculus}},
  booktitle =	{29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
  pages =	{10:1--10:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-262-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{247},
  editor =	{Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.10},
  URN =		{urn:nbn:de:0030-drops-172578},
  doi =		{10.4230/LIPIcs.TIME.2022.10},
  annote =	{Keywords: Gabbay separation, Neighbourhood Logic, Duration Calculus, expanding modalities}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.77
On Uniformization in the Full Binary Tree

Authors: Alexander Rabinovich

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
A function f uniformizes a relation R(X,Y) if R(X,f(X)) holds for every X in the domain of R. The uniformization problem for a logic L asks whether for every L-definable relation there is an L-definable function that uniformizes it. Gurevich and Shelah proved that no Monadic Second-Order (MSO) definable function uniformizes relation "Y is a one element subset of X" in the full binary tree. In other words, there is no MSO definable choice function in the full binary tree. The cross-section of a relation R(X,Y) at D is the set of all E such that R(D,E) holds. Hence, a function that uniformizes R chooses one element from every non-empty cross-section. The relation "Y is a one element subset of X" has finite and countable cross-sections. We prove that in the full binary tree the following theorems hold: ▶ Theorem (Finite cross-sections) If every cross-section of an MSO definable relation is finite, then it has an MSO definable uniformizer. ▶ Theorem (Uncountable cross-section) There is an MSO definable relation R such that every MSO definable relation included in R and with the same domain as R has an uncountable cross-section.
Cite as

Alexander Rabinovich. On Uniformization in the Full Binary Tree. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 77:1-77:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{rabinovich:LIPIcs.MFCS.2022.77,
  author =	{Rabinovich, Alexander},
  title =	{{On Uniformization in the Full Binary Tree}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{77:1--77:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.77},
  URN =		{urn:nbn:de:0030-drops-168757},
  doi =		{10.4230/LIPIcs.MFCS.2022.77},
  annote =	{Keywords: Monadic Second-Order Logic, Uniformization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.36
Degrees of Ambiguity for Parity Tree Automata

Authors: Alexander Rabinovich and Doron Tiferet

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. An automaton is boundedly ambiguous if there is k ∈ ℕ, such that for every input it has at most k accepting computations. We consider Parity Tree Automata (PTA) and prove that the problem whether a PTA is not unambiguous (respectively, is not boundedly ambiguous, not finitely ambiguous) is co-NP complete, and the problem whether a PTA is not countably ambiguous is co-NP hard.
Cite as

Alexander Rabinovich and Doron Tiferet. Degrees of Ambiguity for Parity Tree Automata. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{rabinovich_et_al:LIPIcs.CSL.2021.36,
  author =	{Rabinovich, Alexander and Tiferet, Doron},
  title =	{{Degrees of Ambiguity for Parity Tree Automata}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{36:1--36:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.36},
  URN =		{urn:nbn:de:0030-drops-134709},
  doi =		{10.4230/LIPIcs.CSL.2021.36},
  annote =	{Keywords: automata on infinite trees, degree of ambiguity, omega word automata, parity automata}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.80
Ambiguity Hierarchy of Regular Infinite Tree Languages

Authors: Alexander Rabinovich and Doron Tiferet

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
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 there is k ∈ ℕ, such that for every input it has at most k accepting computations. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. The degree of ambiguity of a regular language is defined in a natural way. A language is k-ambiguous (respectively, boundedly, finitely, countably ambiguous) if it is accepted by a k-ambiguous (respectively, boundedly, finitely, countably ambiguous) automaton. Over finite words every regular language is accepted by a deterministic automaton. Over finite trees every regular language is accepted by an unambiguous automaton. Over ω-words every regular language is accepted by an unambiguous Büchi automaton [Arnold, 1983] and by a deterministic parity automaton. Over infinite trees there are ambiguous languages [Carayol et al., 2010]. We show that over infinite trees there is a hierarchy of degrees of ambiguity: For every k > 1 there are k-ambiguous languages which are not k-1 ambiguous; there are finitely (respectively countably, uncountably) ambiguous languages which are not boundedly (respectively finitely, countably) ambiguous.
Cite as

Alexander Rabinovich and Doron Tiferet. Ambiguity Hierarchy of Regular Infinite Tree Languages. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 80:1-80:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{rabinovich_et_al:LIPIcs.MFCS.2020.80,
  author =	{Rabinovich, Alexander and Tiferet, Doron},
  title =	{{Ambiguity Hierarchy of Regular Infinite Tree Languages}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{80:1--80:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.80},
  URN =		{urn:nbn:de:0030-drops-127495},
  doi =		{10.4230/LIPIcs.MFCS.2020.80},
  annote =	{Keywords: automata on infinite trees, ambiguous automata, monadic second-order logic}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.50
Degrees of Ambiguity of Büchi Tree Automata

Authors: Alexander Rabinovich and Doron Tiferet

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. An automaton is boundedly ambiguous if there is k in N, such that for every input it has at most k accepting computations. We consider nondeterministic Büchi automata (NBA) over infinite trees and prove that it is decidable in polynomial time, whether an automaton is unambiguous, boundedly ambiguous, finitely ambiguous, or countably ambiguous.
Cite as

Alexander Rabinovich and Doron Tiferet. Degrees of Ambiguity of Büchi Tree Automata. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 50:1-50:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{rabinovich_et_al:LIPIcs.FSTTCS.2019.50,
  author =	{Rabinovich, Alexander and Tiferet, Doron},
  title =	{{Degrees of Ambiguity of B\"{u}chi Tree Automata}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{50:1--50:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.50},
  URN =		{urn:nbn:de:0030-drops-116122},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.50},
  annote =	{Keywords: automata on infinite trees, ambiguous automata}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.516
A Proof of Kamp's theorem

Authors: Alexander Rabinovich

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
We provide a simple proof of Kamp's theorem.
Cite as

Alexander Rabinovich. A Proof of Kamp's theorem. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 516-527, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{rabinovich:LIPIcs.CSL.2012.516,
  author =	{Rabinovich, Alexander},
  title =	{{A Proof of Kamp's theorem}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{516--527},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.516},
  URN =		{urn:nbn:de:0030-drops-36945},
  doi =		{10.4230/LIPIcs.CSL.2012.516},
  annote =	{Keywords: Temporal Logic, Monadic Logic, Expressive Completeness}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.307
The Church Synthesis Problem with Metric

Authors: Mark Jenkins, Joël Ouaknine, Alexander Rabinovich, and James Worrell

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
Church's Problem asks for the construction of a procedure which, given a logical specification S(I,O) between input strings I and output strings O, determines whether there exists an operator F that implements the specification in the sense that S(I,F(I)) holds for all inputs I. Buechi and Landweber gave a procedure to solve Church's problem for MSO specifications and operators computable by finite-state automata. We consider extensions of Church's problem in two orthogonal directions: (i) we address the problem in a more general logical setting, where not only the specifications but also the solutions are presented in a logical system; (ii) we consider not only the canonical discrete time domain of the natural numbers, but also the continuous domain of reals. We show that for every fixed bounded length interval of the reals, Church's problem is decidable when specifications and implementations are described in the monadic second-order logics over the reals with order and the +1 function.
Cite as

Mark Jenkins, Joël Ouaknine, Alexander Rabinovich, and James Worrell. The Church Synthesis Problem with Metric. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 307-321, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{jenkins_et_al:LIPIcs.CSL.2011.307,
  author =	{Jenkins, Mark and Ouaknine, Jo\"{e}l and Rabinovich, Alexander and Worrell, James},
  title =	{{The Church Synthesis Problem with Metric}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{307--321},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.307},
  URN =		{urn:nbn:de:0030-drops-32390},
  doi =		{10.4230/LIPIcs.CSL.2011.307},
  annote =	{Keywords: Church's Problem, monadic logic, games, uniformization}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2332
Synthesis of Finite-state and Definable Winning Strategies

Authors: Alexander Rabinovich

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

Abstract
Church's Problem asks for the construction of a procedure which, given a logical specification $\varphi$ on sequence pairs, realizes for any input sequence $I$ an output sequence $O$ such that $(I,O)$ satisfies $\varphi$. McNaughton reduced Church's Problem to a problem about two-player$\omega$-games. B\"uchi and Landweber gave a solution for Monadic Second-Order Logic of Order ($\MLO$) specifications in terms of finite-state strategies. We consider two natural generalizations of the Church problem to countable ordinals: the first deals with finite-state strategies; the second deals with $\MLO$-definable strategies. We investigate games of arbitrary countable length and prove the computability of these generalizations of Church's problem.
Cite as

Alexander Rabinovich. Synthesis of Finite-state and Definable Winning Strategies. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 359-370, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{rabinovich:LIPIcs.FSTTCS.2009.2332,
  author =	{Rabinovich, Alexander},
  title =	{{Synthesis of Finite-state and Definable Winning Strategies}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{359--370},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2332},
  URN =		{urn:nbn:de:0030-drops-23320},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2332},
  annote =	{Keywords: Games of ordinal length, Church Synthesis Problem, Monadic Logic, Composition Method}
}
  • Refine by Author
  • 7 Rabinovich, Alexander
  • 3 Tiferet, Doron
  • 1 Guelev, Dimitar P.
  • 1 Jenkins, Mark
  • 1 Ouaknine, Joël
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Automata over infinite objects
  • 2 Theory of computation → Logic and verification
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Modal and temporal logics

  • Refine by Keyword
  • 3 automata on infinite trees
  • 2 Monadic Logic
  • 2 ambiguous automata
  • 1 Church Synthesis Problem
  • 1 Church's Problem
  • Show More...

  • Refine by Type
  • 8 document

  • Refine by Publication Year
  • 2 2022
  • 1 2009
  • 1 2011
  • 1 2012
  • 1 2019
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact