32 Search Results for "Vardi, Moshe"


Document
Invited Talk
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-dev.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
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-dev.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
AllSAT for Combinational Circuits

Authors: Dror Fried, Alexander Nadel, and Yogev Shalmon

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)


Abstract
Motivated by the need to improve the scalability of Intel’s in-house Static Timing Analysis (STA) tool, we consider the problem of enumerating all the solutions of a single-output combinational Boolean circuit, called AllSAT-CT. While AllSAT-CT is immediately reducible to enumerating the solutions of a Boolean formula in Conjunctive Normal Form (AllSAT-CNF), our experiments had shown that such a reduction, followed by applying state-of-the-art AllSAT-CNF tools, does not scale well on neither our industrial AllSAT-CT instances nor generic circuits, both when the user requires the solutions to be disjoint or when they can be non-disjoint. We focused on understanding the reasons for this phenomenon for the well-known iterative blocking family of AllSAT-CNF algorithms. We realized that existing blocking AllSAT-CNF algorithms fail to generalize efficiently for AllSAT-CT, since they are restricted to Boolean logic. Consequently, we introduce three dedicated AllSAT-CT algorithms that are ternary-logic-aware: a ternary simulation-based algorithm TALE, a dual-rail&MaxSAT-based algorithm MARS, and their combination. Specifically, we introduce in MARS two novel blocking clause generation approaches for the disjoint and non-disjoint cases. We implemented our algorithms in our new tool HALL. We show that HALL scales substantially better than any reduction to existing AllSAT-CNF tools on our industrial STA instances as well as on publicly available families of combinational circuits for both the disjoint and the non-disjoint cases.

Cite as

Dror Fried, Alexander Nadel, and Yogev Shalmon. AllSAT for Combinational Circuits. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{fried_et_al:LIPIcs.SAT.2023.9,
  author =	{Fried, Dror and Nadel, Alexander and Shalmon, Yogev},
  title =	{{AllSAT for Combinational Circuits}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.9},
  URN =		{urn:nbn:de:0030-drops-184717},
  doi =		{10.4230/LIPIcs.SAT.2023.9},
  annote =	{Keywords: AllSAT, SAT, Circuits}
}
Document
Invited Talk
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-dev.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
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-dev.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
Transformations of Boolean Functions

Authors: Jeffrey M. Dudek and Dror Fried

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


Abstract
Boolean functions are characterized by the unique structure of their solution space. Some properties of the solution space, such as the possible existence of a solution, are well sought after but difficult to obtain. To better reason about such properties, we define transformations as functions that change one Boolean function to another while maintaining some properties of the solution space. We explore transformations of Boolean functions, compactly described as Boolean formulas, where the property is to maintain is the number of solutions in the solution spaces. We first discuss general characteristics of such transformations. Next, we reason about the computational complexity of transforming one Boolean formula to another. Finally, we demonstrate the versatility of transformations by extensively discussing transformations of Boolean formulas to "blocks," which are solution spaces in which the set of solutions makes a prefix of the solution space under a lexicographic order of the variables.

Cite as

Jeffrey M. Dudek and Dror Fried. Transformations of Boolean Functions. 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. 39:1-39:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{dudek_et_al:LIPIcs.FSTTCS.2019.39,
  author =	{Dudek, Jeffrey M. and Fried, Dror},
  title =	{{Transformations of Boolean Functions}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{39:1--39: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.39},
  URN =		{urn:nbn:de:0030-drops-116019},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.39},
  annote =	{Keywords: Boolean Formulas, Boolean Functions, Transformations, Model Counting}
}
Document
Alternating Weak Automata from Universal Trees

Authors: Laure Daviaud, Marcin Jurdziński, and Karoliina Lehtinen

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
An improved translation from alternating parity automata on infinite words to alternating weak automata is given. The blow-up of the number of states is related to the size of the smallest universal ordered trees and hence it is quasi-polynomial, and it is polynomial if the asymptotic number of priorities is at most logarithmic in the number of states. This is an exponential improvement on the translation of Kupferman and Vardi (2001) and a quasi-polynomial improvement on the translation of Boker and Lehtinen (2018). Any slightly better such translation would (if - like all presently known such translations - it is efficiently constructive) lead to algorithms for solving parity games that are asymptotically faster in the worst case than the current state of the art (Calude, Jain, Khoussainov, Li, and Stephan, 2017; Jurdziński and Lazić, 2017; and Fearnley, Jain, Schewe, Stephan, and Wojtczak, 2017), and hence it would yield a significant breakthrough.

Cite as

Laure Daviaud, Marcin Jurdziński, and Karoliina Lehtinen. Alternating Weak Automata from Universal Trees. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 18:1-18:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{daviaud_et_al:LIPIcs.CONCUR.2019.18,
  author =	{Daviaud, Laure and Jurdzi\'{n}ski, Marcin and Lehtinen, Karoliina},
  title =	{{Alternating Weak Automata from Universal Trees}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{18:1--18:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.18},
  URN =		{urn:nbn:de:0030-drops-109208},
  doi =		{10.4230/LIPIcs.CONCUR.2019.18},
  annote =	{Keywords: alternating automata, weak automata, B\"{u}chi automata, parity automata, parity games, universal trees}
}
Document
Invited Talk
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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}
}
  • Refine by Author
  • 23 Vardi, Moshe Y.
  • 4 Lohrey, Markus
  • 3 Kupferman, Orna
  • 3 Kuske, Dietrich
  • 2 Downey, Rod
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Computational complexity and cryptography
  • 2 Theory of computation → Design and analysis of algorithms
  • 1 Mathematics of computing → Solvers
  • 1 Software and its engineering
  • 1 Theory of computation → Algorithmic game theory
  • Show More...

  • Refine by Keyword
  • 3 Algorithms
  • 3 Büchi automata
  • 2 Logic
  • 2 Model Counting
  • 2 Theories of infinite structures
  • Show More...

  • Refine by Type
  • 32 document

  • Refine by Publication Year
  • 6 2008
  • 6 2011
  • 3 2018
  • 3 2023
  • 2 2000
  • 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