DROPS

Document

Invited Talk

DOI: 10.4230/LIPIcs.SAT.2024.3

Logical Algorithmics: From Relational Queries to Boolean Reasoning (Invited Talk)

Authors: Moshe Y. Vardi

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract

The standard approach to algorithm development is to focus on a specific problem and develop for it a specific algorithm. Codd’s introduction of the relational model in 1970 included two fundamental ideas: (1) relations provide a universal data representation formalism, and (2) relational databases can be queried using first-order logic. Realizing these ideas required the development of a meta-algorithm, which takes a declarative query and executes it with respect to a database. In this talk, I will describe this approach, which I call Logical Algorithmics, in detail, and trace a decades-long path from the comoutational complexity theory of relational queries to recent tools for Boolean reasoning.

Cite as

Moshe Y. Vardi. Logical Algorithmics: From Relational Queries to Boolean Reasoning (Invited Talk). In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{vardi:LIPIcs.SAT.2024.3,
  author =	{Vardi, Moshe Y.},
  title =	{{Logical Algorithmics: From Relational Queries to Boolean Reasoning}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.3},
  URN =		{urn:nbn:de:0030-drops-205253},
  doi =		{10.4230/LIPIcs.SAT.2024.3},
  annote =	{Keywords: Logic, Algorithms}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.CSL.2024.6

Logical Algorithmics: From Theory to Practice (Invited Talk)

Authors: Moshe Y. Vardi

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract

The standard approach to algorithm development is to focus on a specific problem and develop for it a specific algorithm. Codd’s introduction of the relational model in 1970 included two fundamental ideas: (1) Relations provide a universal data representation formalism, and (2) Relational databases can be queried using first-order logic. Realizing these ideas required the development of a meta-algorithm, which takes a declarative query and executes it with respect to a database. In this talk, I will describe this approach, which I call Logical Algorithmics, in detail, and explore its profound ramification.

Cite as

Moshe Y. Vardi. Logical Algorithmics: From Theory to Practice (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, p. 6:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{vardi:LIPIcs.CSL.2024.6,
  author =	{Vardi, Moshe Y.},
  title =	{{Logical Algorithmics: From Theory to Practice}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{6:1--6:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.6},
  URN =		{urn:nbn:de:0030-drops-196494},
  doi =		{10.4230/LIPIcs.CSL.2024.6},
  annote =	{Keywords: Logic, Algorithms}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2023.37

Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata

Authors: Yong Li, Sven Schewe, and Moshe Y. Vardi

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract

We introduce a method for translating an alternating weak Büchi automaton (AWA), which corresponds to a Linear Dynamic Logic (LDL) formula, to an unambiguous Büchi automaton (UBA). Our translations generalise constructions for Linear Temporal Logic (LTL), a less expressive specification language than LDL. In classical constructions, LTL formulas are first translated to alternating very weak automata (AVAs) - automata that have only singleton strongly connected components (SCCs); the AVAs are then handled by efficient disambiguation procedures. However, general AWAs can have larger SCCs, which complicates disambiguation. Currently, the only available disambiguation procedure has to go through an intermediate construction of nondeterministic Büchi automata (NBAs), which would incur an exponential blow-up of its own. We introduce a translation from general AWAs to UBAs with a singly exponential blow-up, which also immediately provides a singly exponential translation from LDL to UBAs. Interestingly, the complexity of our translation is smaller than the best known disambiguation algorithm for NBAs (broadly (0.53n)ⁿ vs. (0.76n)ⁿ), while the input of our construction can be exponentially more succinct.

Cite as

Yong Li, Sven Schewe, and Moshe Y. Vardi. Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.CONCUR.2023.37,
  author =	{Li, Yong and Schewe, Sven and Vardi, Moshe Y.},
  title =	{{Singly Exponential Translation of Alternating Weak B\"{u}chi Automata to Unambiguous B\"{u}chi Automata}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{37:1--37:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.37},
  URN =		{urn:nbn:de:0030-drops-190313},
  doi =		{10.4230/LIPIcs.CONCUR.2023.37},
  annote =	{Keywords: B\"{u}chi automata, unambiguous automata, alternation, weak, disambiguation}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.STACS.2023.3

Logical Algorithmics: From Theory to Practice (Invited Talk)

Authors: Moshe Y. Vardi

Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)

Abstract

The standard approach to algorithm development is to focus on a specific problem and develop for it a specific algorithm. Codd’s introduction of the relational model in 1970 included two fundamental ideas: (1) Relations provide a universal data representation formalism, and (2) Relational databases can be queried using first-order logic. Realizing these ideas required the development of a meta-algorithm, which takes a declarative query and executes it with respect to a database. In this talk, I will describe this approach, which I call Logical Algorithmics, in detail, and explore its profound ramification.

Cite as

Moshe Y. Vardi. Logical Algorithmics: From Theory to Practice (Invited Talk). In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{vardi:LIPIcs.STACS.2023.3,
  author =	{Vardi, Moshe Y.},
  title =	{{Logical Algorithmics: From Theory to Practice}},
  booktitle =	{40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-266-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{254},
  editor =	{Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.3},
  URN =		{urn:nbn:de:0030-drops-176555},
  doi =		{10.4230/LIPIcs.STACS.2023.3},
  annote =	{Keywords: Logic, Algorithms}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.TIME.2022.1

Linear Temporal Logic: From Infinite to Finite Horizon (Invited Talk)

Authors: Moshe Y. Vardi

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

Abstract

Linear Temporal Logic (LTL), proposed in 1977 by Amir Pnueli for reasoning about ongoing programs, was defined over infinite traces. The motivation for this was the desire to model arbitrarily long computations. While this approach has been highly successful in the context of model checking, it has been less successful in the context of reactive synthesis, due to the chalenging algorithmics of infinite-horizon temporal synthesis. In this talk we show that focusing on finite-horizon temporal synthesis offers enough algorithmic advantages to compensate for the loss in expressiveness. In fact, finite-horizon reasonings is useful even in the context of infinite-horizon applications.

Cite as

Moshe Y. Vardi. Linear Temporal Logic: From Infinite to Finite Horizon (Invited Talk). In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{vardi:LIPIcs.TIME.2022.1,
  author =	{Vardi, Moshe Y.},
  title =	{{Linear Temporal Logic: From Infinite to Finite Horizon}},
  booktitle =	{29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
  pages =	{1:1--1:1},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.1},
  URN =		{urn:nbn:de:0030-drops-172481},
  doi =		{10.4230/LIPIcs.TIME.2022.1},
  annote =	{Keywords: Temporal Logic}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.CONCUR.2018.1

The Siren Song of Temporal Synthesis (Invited Talk)

Authors: Moshe Y. Vardi

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract

One of the most significant developments in the area of design verification over the last three decade is the development of algorithmic methods for verifying temporal specification of finite-state designs. A frequent criticism against this approach, however, is that verification is done after significant resources have already been invested in the development of the design. Since designs invariably contains errors, verification simply becomes part of the debugging process. The critics argue that the desired goal is to use temporal specification in the design development process in order to guarantee the development of correct designs. This is called temporal synthesis. In this talk I will review 60 years of research on the temporal synthesis problem, describe the automata-theoretic approach developed to solve this problem, and describe both successes and failures of this research program [Zhu et al., 2017a and 2017b].

Cite as

Moshe Y. Vardi. The Siren Song of Temporal Synthesis (Invited Talk). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{vardi:LIPIcs.CONCUR.2018.1,
  author =	{Vardi, Moshe Y.},
  title =	{{The Siren Song of Temporal Synthesis}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.1},
  URN =		{urn:nbn:de:0030-drops-95393},
  doi =		{10.4230/LIPIcs.CONCUR.2018.1},
  annote =	{Keywords: Formal Methods, Temporal Synthesis}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2017.38

Flow Games

Authors: Orna Kupferman, Gal Vardi, and Moshe Y. Vardi

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract

In the traditional maximal-flow problem, the goal is to transfer maximum flow in a network by directing, in each vertex in the network, incoming flow into outgoing edges. While the problem has been extensively used in order to optimize the performance of networks in numerous application areas, it corresponds to a setting in which the authority has control on all vertices of the network. Today's computing environment involves parties that should be considered adversarial. We introduce and study {\em flow games}, which capture settings in which the authority can control only part of the vertices. In these games, the vertices are partitioned between two players: the authority and the environment. While the authority aims at maximizing the flow, the environment need not cooperate. We argue that flow games capture many modern settings, such as partially-controlled pipe or road systems or hybrid software-defined communication networks. We show that the problem of finding the maximal flow as well as an optimal strategy for the authority in an acyclic flow game is $\Sigma_2^P$-complete, and is already $\Sigma_2^P$-hard to approximate. We study variants of the game: a restriction to strategies that ensure no loss of flow, an extension to strategies that allow non-integral flows, which we prove to be stronger, and a dynamic setting in which a strategy for a vertex is chosen only once flow reaches the vertex. We discuss additional variants and their applications, and point to several interesting open problems.

Cite as

Orna Kupferman, Gal Vardi, and Moshe Y. Vardi. Flow Games. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 38:1-38:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.FSTTCS.2017.38,
  author =	{Kupferman, Orna and Vardi, Gal and Vardi, Moshe Y.},
  title =	{{Flow Games}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{38:1--38:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.38},
  URN =		{urn:nbn:de:0030-drops-83738},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.38},
  annote =	{Keywords: Flow networks, Two-player Games, Algorithms}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2017.41

On Hashing-Based Approaches to Approximate DNF-Counting

Authors: Kuldeep S. Meel, Aditya A. Shrotri, and Moshe Y. Vardi

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract

Propositional model counting is a fundamental problem in artificial intelligence with a wide variety of applications, such as probabilistic inference, decision making under uncertainty, and probabilistic databases. Consequently, the problem is of theoretical as well as practical interest. When the constraints are expressed as DNF formulas, Monte Carlo-based techniques have been shown to provide a fully polynomial randomized approximation scheme (FPRAS). For CNF constraints, hashing-based approximation techniques have been demonstrated to be highly successful. Furthermore, it was shown that hashing-based techniques also yield an FPRAS for DNF counting without usage of Monte Carlo sampling. Our analysis, however, shows that the proposed hashing-based approach to DNF counting provides poor time complexity compared to the Monte Carlo-based DNF counting techniques. Given the success of hashing-based techniques for CNF constraints, it is natural to ask: Can hashing-based techniques provide an efficient FPRAS for DNF counting? In this paper, we provide a positive answer to this question. To this end, we introduce two novel algorithmic techniques: Symbolic Hashing and Stochastic Cell Counting, along with a new hash family of Row-Echelon hash functions. These innovations allow us to design a hashing-based FPRAS for DNF counting of similar complexity (up to polylog factors) as that of prior works. Furthermore, we expect these techniques to have potential applications beyond DNF counting.

Cite as

Kuldeep S. Meel, Aditya A. Shrotri, and Moshe Y. Vardi. On Hashing-Based Approaches to Approximate DNF-Counting. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 41:1-41:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{meel_et_al:LIPIcs.FSTTCS.2017.41,
  author =	{Meel, Kuldeep S. and Shrotri, Aditya A. and Vardi, Moshe Y.},
  title =	{{On Hashing-Based Approaches to Approximate DNF-Counting}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{41:1--41:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.41},
  URN =		{urn:nbn:de:0030-drops-84073},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.41},
  annote =	{Keywords: Model Counting, Approximation, DNF, Hash Functions}
}

Document

DOI: 10.4230/LIPIcs.ICDT.2015.177

Regular Queries on Graph Databases

Authors: Juan L. Reutter, Miguel Romero, and Moshe Y. Vardi

Published in: LIPIcs, Volume 31, 18th International Conference on Database Theory (ICDT 2015)

Abstract

Graph databases are currently one of the most popular paradigms for storing data. One of the key conceptual differences between graph and relational databases is the focus on navigational queries that ask whether some nodes are connected by paths satisfying certain restrictions. This focus has driven the definition of several different query languages and the subsequent study of their fundamental properties. We define the graph query language of Regular Queries, which is a natural extension of unions of conjunctive 2-way regular path queries (UC2RPQs) and unions of conjunctive nested 2-way regular path queries (UCN2RPQs). Regular queries allow expressing complex regular patterns between nodes. We formalize regular queries as nonrecursive Datalog programs with transitive closure rules. This language has been previously considered, but its algorithmic properties are not well understood. Our main contribution is to show elementary tight bounds for the containment problem for regular queries. Specifically, we show that this problem is 2EXPSPACE-complete. For all extensions of regular queries known to date, the containment problem turns out to be non-elementary. Together with the fact that evaluating regular queries is not harder than evaluating UCN2RPQs, our results show that regular queries achieve a good balance between expressiveness and complexity, and constitute a well-behaved class that deserves further investigation.

Cite as

Juan L. Reutter, Miguel Romero, and Moshe Y. Vardi. Regular Queries on Graph Databases. In 18th International Conference on Database Theory (ICDT 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 31, pp. 177-194, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{reutter_et_al:LIPIcs.ICDT.2015.177,
  author =	{Reutter, Juan L. and Romero, Miguel and Vardi, Moshe Y.},
  title =	{{Regular Queries on Graph Databases}},
  booktitle =	{18th International Conference on Database Theory (ICDT 2015)},
  pages =	{177--194},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-79-8},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{31},
  editor =	{Arenas, Marcelo and Ugarte, Mart{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2015.177},
  URN =		{urn:nbn:de:0030-drops-49842},
  doi =		{10.4230/LIPIcs.ICDT.2015.177},
  annote =	{Keywords: graph databases, conjunctive regular path queries, regular queries, containment.}
}

Document

DOI: 10.4230/DagRep.4.6.29

Design and Synthesis from Components (Dagstuhl Seminar 14232)

Authors: Jakob Rehof and Moshe Y. Vardi

Published in: Dagstuhl Reports, Volume 4, Issue 6 (2015)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 14232 "Design and Synthesis from Components" which took place from June 1st to June 6th, 2014. The seminar aimed at bringing together researchers from the component-oriented design community, researchers working on interface theories, and researchers working in synthesis, in order to explore the use of component- and interface design in program synthesis. The seminar program consisted of 6 tutorial talks (1 hour) and 16 contributed talks (30 mins) as well as joint discussion sessions. This report documents the abstracts of the talks as well as summaries of discussion sessions.

Cite as

Jakob Rehof and Moshe Y. Vardi. Design and Synthesis from Components (Dagstuhl Seminar 14232). In Dagstuhl Reports, Volume 4, Issue 6, pp. 29-47, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{rehof_et_al:DagRep.4.6.29,
  author =	{Rehof, Jakob and Vardi, Moshe Y.},
  title =	{{Design and Synthesis from Components (Dagstuhl Seminar 14232)}},
  pages =	{29--47},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{6},
  editor =	{Rehof, Jakob and Vardi, Moshe Y.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.6.29},
  URN =		{urn:nbn:de:0030-drops-46839},
  doi =		{10.4230/DagRep.4.6.29},
  annote =	{Keywords: Component design, Component-based synthesis}
}

Document

DOI: 10.4230/DagRep.2.11.20

Publication Culture in Computing Research (Dagstuhl Perspectives Workshop 12452)

Authors: Kurt Mehlhorn, Moshe Y. Vardi, and Marc Herbstritt

Published in: Dagstuhl Reports, Volume 2, Issue 11 (2013)

Abstract

The dissemination of research results is an integral part of research and hence a crucial component for any scientific discipline. In the area of computing research, there have been raised concerns recently about its publication culture, most notably by highlighting the high priority of conferences (compared to journals in other disciplines) and -- from an economic viewpoint -- the costs of preparing and accessing research results. The Dagstuhl Perspectives Workshop 12452 ``Publication Culture in Computing Research'' aimed at discussing the main problems with a selected group of researchers and practitioners. The goal was to identify and classify the current problems and to suggest potential remedies. The group of participants was selected in a way such that a wide spectrum of opinions would be presented. This lead to intensive discussions. The workshop is seen as an important step in the ongoing discussion. As a main result, the main problem roots were identified and potential solutions were discussed. The insights will be part of an upcoming manifesto on Publication Culture in Computing Research.

Cite as

Kurt Mehlhorn, Moshe Y. Vardi, and Marc Herbstritt. Publication Culture in Computing Research (Dagstuhl Perspectives Workshop 12452). In Dagstuhl Reports, Volume 2, Issue 11, pp. 20-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{mehlhorn_et_al:DagRep.2.11.20,
  author =	{Mehlhorn, Kurt and Vardi, Moshe Y. and Herbstritt, Marc},
  title =	{{Publication Culture in Computing Research (Dagstuhl Perspectives Workshop 12452)}},
  pages =	{20--44},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{2},
  number =	{11},
  editor =	{Mehlhorn, Kurt and Vardi, Moshe Y. and Herbstritt, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.2.11.20},
  URN =		{urn:nbn:de:0030-drops-39778},
  doi =		{10.4230/DagRep.2.11.20},
  annote =	{Keywords: scholarly publishing, conference, journal, peer review, open archive, open access, indexing, research evaluation}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSTTCS.2011.3

Constraints, Graphs, Algebra, Logic, and Complexity (Invited Talk)

Authors: Moshe Y. Vardi

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

Abstract

A large class of problems in AI and other areas of computer science can be viewed as constraint-satisfaction problems. This includes problems in database query optimization, machine vision, belief maintenance, scheduling, temporal reasoning, type reconstruction, graph theory, and satisfiability. All of these problems can be recast as questions regarding the existence of homomorphisms between two directed graphs. It is well-known that the constraint-satisfaction problem is NP-complete. This motivated an extensive research program into identify tractable cases of constraint satisfaction. This research proceeds along two major lines. The first line of research focuses on non-uniform constraint satisfaction, where the target graph is fixed. The goal is to identify those target graphs that give rise to a tractable constraint-satisfaction problem. The second line of research focuses on identifying large classes of source graphs for which constraint-satisfaction is tractable. We show in how tools from graph theory, universal algebra, logic, and complexity theory, shed light on the tractability of constraint satisfaction.

Cite as

Moshe Y. Vardi. Constraints, Graphs, Algebra, Logic, and Complexity (Invited Talk). In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, p. 3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{vardi:LIPIcs.FSTTCS.2011.3,
  author =	{Vardi, Moshe Y.},
  title =	{{Constraints, Graphs, Algebra, Logic, and Complexity}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{3--3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.3},
  URN =		{urn:nbn:de:0030-drops-33580},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.3},
  annote =	{Keywords: constraint satisfaction, NP completeness, dichotomy}
}

Document

DOI: 10.4230/DagMan.1.1.21

Modeling, Analysis, and Verification - The Formal Methods Manifesto 2010 (Dagstuhl Perspectives Workshop 10482)

Authors: Jörg Kreiker, Andrzej Tarlecki, Moshe Y. Vardi, and Reinhard Wilhelm

Published in: Dagstuhl Manifestos, Volume 1, Issue 1 (2011)

Abstract

This manifesto represents the results of the Dagstuhl Perspectives Workshop 10482 "Formal Methods – Just a Euro-Science?" held from November 30 to December 3, 2010 at Schloss Dagstuhl, Germany. We strive to clarify the terminology and categorize the abundance of concepts and methods in order to reduce misunderstandings among the involved research community and in communication with industry. We discuss the industrial acceptance of formal methods and how to increase it by targeted research and improved education. Finally, we state a few challenges and provide perspectives of the field. This document is opinionated in nature and biased towards the experiences and views of the participants listed in the appendix, further distilled by the authors.

Cite as

Jörg Kreiker, Andrzej Tarlecki, Moshe Y. Vardi, and Reinhard Wilhelm. Modeling, Analysis, and Verification - The Formal Methods Manifesto 2010 (Dagstuhl Perspectives Workshop 10482). In Dagstuhl Manifestos, Volume 1, Issue 1, pp. 21-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@Article{kreiker_et_al:DagMan.1.1.21,
  author =	{Kreiker, J\"{o}rg and Tarlecki, Andrzej and Vardi, Moshe Y. and Wilhelm, Reinhard},
  title =	{{Modeling, Analysis, and Verification - The Formal Methods Manifesto 2010 (Dagstuhl Perspectives Workshop 10482)}},
  pages =	{21--40},
  journal =	{Dagstuhl Manifestos},
  ISSN =	{2193-2433},
  year =	{2011},
  volume =	{1},
  number =	{1},
  editor =	{Kreiker, J\"{o}rg and Tarlecki, Andrzej and Vardi, Moshe Y. and Wilhelm, Reinhard},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagMan.1.1.21},
  URN =		{urn:nbn:de:0030-drops-32121},
  doi =		{10.4230/DagMan.1.1.21},
  annote =	{Keywords: Formal methods, Verification, Analysis, Modeling, Design for Verifiability}
}

Document

DOI: 10.4230/LIPIcs.CSL.2011.3

Branching vs. Linear Time: Semantical Perspective

Authors: Moshe Y. Vardi

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

Abstract

The discussion of the relative merits of linear- versus branching-time frameworks goes back to the early 1980s. We revisit here this issue from a fresh perspective and postulate three principles that we view as fundamental to any discussion of process equivalence. We show that our principles yield a unique notion of process equivalence, which is trace based, rather than tree based.

Cite as

Moshe Y. Vardi. Branching vs. Linear Time: Semantical Perspective. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, p. 3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{vardi:LIPIcs.CSL.2011.3,
  author =	{Vardi, Moshe Y.},
  title =	{{Branching vs. Linear Time: Semantical Perspective}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{3--3},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.3},
  URN =		{urn:nbn:de:0030-drops-32173},
  doi =		{10.4230/LIPIcs.CSL.2011.3},
  annote =	{Keywords: linear time, branching time, process equivalence, contextual equivalence}
}

Document

DOI: 10.4230/LIPIcs.CSL.2011.248

Unifying Büchi Complementation Constructions

Authors: Seth Fogarty, Orna Kupferman, Moshe Y. Vardi, and Thomas Wilke

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

Abstract

Complementation of Buechi automata, required for checking automata containment, is of major theoretical and practical interest in formal verification. We consider two recent approaches to complementation. The first is the rank-based approach of Kupferman and Vardi, which operates over a DAG that embodies all runs of the automaton. This approach is based on the observation that the vertices of this DAG can be ranked in a certain way, termed an odd ranking, iff all runs are rejecting. The second is the slice-based approach of Kahler and Wilke. This approach tracks levels of "split trees" - run trees in which only essential information about the history of each run is maintained. While the slice-based construction is conceptually simple, the complementing automata it generates are exponentially larger than those of the recent rank-based construction of Schewe, and it suffers from the difficulty of symbolically encoding levels of split trees. In this work we reformulate the slice-based approach in terms of run DAGs and preorders over states. In doing so, we begin to draw parallels between the rank-based and slice-based approaches. Through deeper analysis of the slice-based approach, we strongly restrict the nondeterminism it generates. We are then able to employ the slice-based approach to provide a new odd ranking, called a retrospective ranking, that is different from the one provided by Kupferman and Vardi. This new ranking allows us to construct a deterministic-in-the-limit rank-based automaton with a highly restricted transition function. Further, by phrasing the slice-based approach in terms of ranks, our approach affords a simple symbolic encoding and achieves Schewe's tight bound.

Cite as

Seth Fogarty, Orna Kupferman, Moshe Y. Vardi, and Thomas Wilke. Unifying Büchi Complementation Constructions. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 248-263, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{fogarty_et_al:LIPIcs.CSL.2011.248,
  author =	{Fogarty, Seth and Kupferman, Orna and Vardi, Moshe Y. and Wilke, Thomas},
  title =	{{Unifying B\"{u}chi Complementation Constructions}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{248--263},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.248},
  URN =		{urn:nbn:de:0030-drops-32357},
  doi =		{10.4230/LIPIcs.CSL.2011.248},
  annote =	{Keywords: B\"{u}chi automata, complementation, ranks, determinism in the limit}
}

Document

DOI: 10.4230/LIPIcs.CSL.2011.412

Synthesis from Probabilistic Components

Authors: Yoad Lustig, Sumit Nain, and Moshe Y. Vardi

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

Abstract

Synthesis is the automatic construction of a system from its specification. In classical synthesis algorithms, it is always assumed that the system is "constructed from scratch" rather than composed from reusable components. This, of course, rarely happens in real life, where almost every non-trivial commercial software system relies heavily on using libraries of reusable components. Furthermore, other contexts, such as web-service orchestration, can be modeled as synthesis of a system from a library of components. Recently, Lustig and Vardi introduced dataflow and control-flow synthesis from libraries of reusable components. They proved that dataflow synthesis is undecidable, while control-flow synthesis is decidable. In this work, we consider the problem of control-flow synthesis from libraries of probabilistic components. We show that this more general problem is also decidable.

Cite as

Yoad Lustig, Sumit Nain, and Moshe Y. Vardi. Synthesis from Probabilistic Components. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 412-427, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{lustig_et_al:LIPIcs.CSL.2011.412,
  author =	{Lustig, Yoad and Nain, Sumit and Vardi, Moshe Y.},
  title =	{{Synthesis from Probabilistic Components}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{412--427},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.412},
  URN =		{urn:nbn:de:0030-drops-32461},
  doi =		{10.4230/LIPIcs.CSL.2011.412},
  annote =	{Keywords: temporal synthesis, probabilistic components}
}

Document

DOI: 10.4230/LIPIcs.STACS.2011.615

Temporal Synthesis for Bounded Systems and Environments

Authors: Orna Kupferman, Yoad Lustig, Moshe Y. Vardi, and Mihalis Yannakakis

Published in: LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)

Abstract

Temporal synthesis is the automated construction of a system from its temporal specification. It is by now realized that requiring the synthesized system to satisfy the specifications against all possible environments may be too demanding, and, dually, allowing all systems may be not demanding enough. In this work we study bounded temporal synthesis, in which bounds on the sizes of the state space of the system and the environment are additional parameters to the synthesis problem. This study is motivated by the fact that such bounds may indeed change the answer to the synthesis problem, as well as the theoretical and computational aspects of the synthesis problem. In particular, a finer analysis of synthesis, which takes system and environment sizes into account, yields deeper insight into the quantificational structure of the synthesis problem and the relationship between strong synthesis -- there exists a system such that for all environments, the specification holds, and weak synthesis -- for all environments there exists a system such that the specification holds. We first show that unlike the unbounded setting, where determinacy of regular games implies that strong and weak synthesis coincide, these notions do not coincide in the bounded setting. We then turn to study the complexity of deciding strong and weak synthesis. We show that bounding the size of the system or both the system and the environment, turns the synthesis problem into a search problem, and one cannot expect to do better than brute-force search. In particular, the synthesis problem for bounded systems and environment is Sigma^P_2-complete (in terms of the bounds, for a specification given by a deterministic automaton). We also show that while bounding the environment may lead to the synthesis of specifications that are otherwise unrealizable, such relaxation of the problem comes at a high price from a complexity-theoretic point of view.

Cite as

Orna Kupferman, Yoad Lustig, Moshe Y. Vardi, and Mihalis Yannakakis. Temporal Synthesis for Bounded Systems and Environments. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 9, pp. 615-626, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.STACS.2011.615,
  author =	{Kupferman, Orna and Lustig, Yoad and Vardi, Moshe Y. and Yannakakis, Mihalis},
  title =	{{Temporal Synthesis for Bounded Systems and Environments}},
  booktitle =	{28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)},
  pages =	{615--626},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-25-5},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{9},
  editor =	{Schwentick, Thomas and D\"{u}rr, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.615},
  URN =		{urn:nbn:de:0030-drops-30481},
  doi =		{10.4230/LIPIcs.STACS.2011.615},
  annote =	{Keywords: temporal synthesis}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2010.133

Reasoning About Strategies

Authors: Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi

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

Abstract

In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between open entities and express that the system is correct no matter how the environment behaves. An important contribution in this context is given by modal logics for strategic ability, in the setting of multi-agent games, such as ATL, ATL*, and the like. Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by SL-CHP, with the aim of getting a powerful framework for reasoning explicitly about strategies. SL-CHP is obtained by using first-order quantifications over strategies and it has been investigated in the specific setting of two-agents turn-based game structures where a non-elementary model-checking algorithm has been provided. While SL-CHP is a very expressive logic, we claim that it does not fully capture the strategic aspects of multi-agent systems. In this paper, we introduce and study a more general strategy logic, denoted SL, for reasoning about strategies in multi-agent concurrent systems. We prove that SL strictly includes SL-CHP, while maintaining a decidable model-checking problem. Indeed, we show that it is 2ExpTime-complete, thus not harder than that for ATL* and a remarkable improvement of the same problem for SL-CHP. We also consider the satisfiability problem and show that it is undecidable already for the sub-logic SL-CHP under the concurrent game semantics.

Cite as

Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi. Reasoning About Strategies. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 133-144, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{mogavero_et_al:LIPIcs.FSTTCS.2010.133,
  author =	{Mogavero, Fabio and Murano, Aniello and Vardi, Moshe Y.},
  title =	{{Reasoning About Strategies}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{133--144},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.133},
  URN =		{urn:nbn:de:0030-drops-28597},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.133},
  annote =	{Keywords: open systems, multi-agent systems, verification, strategy quantifier, alternating temporal logic, model-checking}
}

Document

DOI: 10.4230/DagSemProc.07441.1

07441 Abstracts Collection – Algorithmic-Logical Theory of Infinite Structures

Authors: Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, and Moshe Y. Vardi

Published in: Dagstuhl Seminar Proceedings, Volume 7441, Algorithmic-Logical Theory of Infinite Structures (2008)

Abstract

From 28.10. to 02.11.2007, the Dagstuhl Seminar 07441 ``Algorithmic-Logical Theory of Infinite Structures'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, and Moshe Y. Vardi. 07441 Abstracts Collection – Algorithmic-Logical Theory of Infinite Structures. In Algorithmic-Logical Theory of Infinite Structures. Dagstuhl Seminar Proceedings, Volume 7441, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{downey_et_al:DagSemProc.07441.1,
  author =	{Downey, Rod and Khoussainov, Bakhadyr and Kuske, Dietrich and Lohrey, Markus and Vardi, Moshe Y.},
  title =	{{07441 Abstracts Collection – Algorithmic-Logical Theory of Infinite Structures}},
  booktitle =	{Algorithmic-Logical Theory of Infinite Structures},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7441},
  editor =	{Rod Downey and Bakhadyr Khoussainov and Dietrich Kuske and Markus Lohrey and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07441.1},
  URN =		{urn:nbn:de:0030-drops-14122},
  doi =		{10.4230/DagSemProc.07441.1},
  annote =	{Keywords: Theories of infinite structures , computable model theory and automatic structures , model checking infinite systems}
}

Document

DOI: 10.4230/DagSemProc.07441.2

07441 Summary – Algorithmic-Logical Theory of Infinite Structures

Authors: Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, and Moshe Y. Vardi

Published in: Dagstuhl Seminar Proceedings, Volume 7441, Algorithmic-Logical Theory of Infinite Structures (2008)

Abstract

One of the important research fields of theoretical and applied computer science and mathematics is the study of algorithmic, logical and model theoretic properties of structures and their interactions. By a structure we mean typical objects that arise in computer science and mathematics such as data structures, programs, transition systems, graphs, large databases, XML documents, algebraic systems including groups, integers, fields, Boolean algebras and so on.

Cite as

Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, and Moshe Y. Vardi. 07441 Summary – Algorithmic-Logical Theory of Infinite Structures. In Algorithmic-Logical Theory of Infinite Structures. Dagstuhl Seminar Proceedings, Volume 7441, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{downey_et_al:DagSemProc.07441.2,
  author =	{Downey, Rod and Khoussainov, Bakhadyr and Kuske, Dietrich and Lohrey, Markus and Vardi, Moshe Y.},
  title =	{{07441 Summary – Algorithmic-Logical Theory of Infinite Structures}},
  booktitle =	{Algorithmic-Logical Theory of Infinite Structures},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7441},
  editor =	{Rod Downey and Bakhadyr Khoussainov and Dietrich Kuske and Markus Lohrey and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07441.2},
  URN =		{urn:nbn:de:0030-drops-14111},
  doi =		{10.4230/DagSemProc.07441.2},
  annote =	{Keywords: Theories of infinite structures , computable model theory and automatic structures , model checking infinite systems}
}

Document

DOI: 10.4230/DagSemProc.05241.1

05241 Abstracts Collection – Synthesis and Planning

Authors: Henry Kautz, Wolfgang Thomas, and Moshe Y. Vardi

Published in: Dagstuhl Seminar Proceedings, Volume 5241, Synthesis and Planning (2006)

Abstract

From 12.06.05 to 17.06.2005 the Dagstuhl Seminar 05241 ``Synthesis and Planning'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Henry Kautz, Wolfgang Thomas, and Moshe Y. Vardi. 05241 Abstracts Collection – Synthesis and Planning. In Synthesis and Planning. Dagstuhl Seminar Proceedings, Volume 5241, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{kautz_et_al:DagSemProc.05241.1,
  author =	{Kautz, Henry and Thomas, Wolfgang and Vardi, Moshe Y.},
  title =	{{05241 Abstracts Collection – Synthesis and Planning}},
  booktitle =	{Synthesis and Planning},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5241},
  editor =	{Henry Kautz and Wolfgang Thomas and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05241.1},
  URN =		{urn:nbn:de:0030-drops-4531},
  doi =		{10.4230/DagSemProc.05241.1},
  annote =	{Keywords: AI planning, controller synthesis, partially observed domains, reactive computation, program analysis, games, model checking, satisfiability, Markov decision processes}
}

Document

DOI: 10.4230/DagSemProc.05241.2

05241 Executive Summary – Synthesis and Planning

Authors: Henry Kautz, Wolfgang Thomas, and Moshe Y. Vardi

Published in: Dagstuhl Seminar Proceedings, Volume 5241, Synthesis and Planning (2006)

Abstract

This seminar has brought together researchers working in two complementary fields: automatic synthesis of (control) programs, and methods for devising planning algorithms in artifical intelligence (AI). This combines a strong thread of current research in automata theory with an area of possible but so far unexplored applications.

Cite as

Henry Kautz, Wolfgang Thomas, and Moshe Y. Vardi. 05241 Executive Summary – Synthesis and Planning. In Synthesis and Planning. Dagstuhl Seminar Proceedings, Volume 5241, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{kautz_et_al:DagSemProc.05241.2,
  author =	{Kautz, Henry and Thomas, Wolfgang and Vardi, Moshe Y.},
  title =	{{05241 Executive Summary – Synthesis and Planning}},
  booktitle =	{Synthesis and Planning},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5241},
  editor =	{Henry Kautz and Wolfgang Thomas and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05241.2},
  URN =		{urn:nbn:de:0030-drops-4527},
  doi =		{10.4230/DagSemProc.05241.2},
  annote =	{Keywords: Synthesis, planning}
}

Document

DOI: 10.4230/DagSemRep.379

Probabilistic Methods in Verification and Planning (Dagstuhl Seminar 03201)

Authors: Craig Boutilier, Boudewijn Haverkort, Marta Kwiatkowska, and Moshe Y. Vardi

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract

Cite as

Craig Boutilier, Boudewijn Haverkort, Marta Kwiatkowska, and Moshe Y. Vardi. Probabilistic Methods in Verification and Planning (Dagstuhl Seminar 03201). Dagstuhl Seminar Report 379, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2003)

Copy BibTex To Clipboard

@TechReport{boutilier_et_al:DagSemRep.379,
  author =	{Boutilier, Craig and Haverkort, Boudewijn and Kwiatkowska, Marta and Vardi, Moshe Y.},
  title =	{{Probabilistic Methods in Verification and Planning (Dagstuhl Seminar 03201)}},
  pages =	{1--8},
  ISSN =	{1619-0203},
  year =	{2003},
  type = 	{Dagstuhl Seminar Report},
  number =	{379},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.379},
  URN =		{urn:nbn:de:0030-drops-152590},
  doi =		{10.4230/DagSemRep.379},
}

Document

DOI: 10.4230/DagSemRep.326

Exploration of Large State Spaces (Dagstuhl Seminar 01451)

Authors: Tom L. Dean, Bernhard Nebel, and Moshe Y. Vardi

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract

Cite as

Tom L. Dean, Bernhard Nebel, and Moshe Y. Vardi. Exploration of Large State Spaces (Dagstuhl Seminar 01451). Dagstuhl Seminar Report 326, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2002)

Copy BibTex To Clipboard

@TechReport{dean_et_al:DagSemRep.326,
  author =	{Dean, Tom L. and Nebel, Bernhard and Vardi, Moshe Y.},
  title =	{{Exploration of Large State Spaces (Dagstuhl Seminar 01451)}},
  pages =	{1--22},
  ISSN =	{1619-0203},
  year =	{2002},
  type = 	{Dagstuhl Seminar Report},
  number =	{326},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.326},
  URN =		{urn:nbn:de:0030-drops-152090},
  doi =		{10.4230/DagSemRep.326},
}

Search Results

Documents authored by Vardi, Moshe

Vardi, Moshe Y.

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Vardi, Moshe

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message