Moshe Y. Vardi

AAAI Conference 2025 Conference Paper

LTLf Synthesis Under Unreliable Input

• Christian Hagemeier
• Giuseppe De Giacomo
• Moshe Y. Vardi

We study the problem of realizing strategies for an LTLf goal specification while ensuring that at least an LTLf backup specification is satisfied in case of unreliability of certain input variables. We formally define the problem and characterize its worst-case complexity as 2EXPTIME-complete, like standard LTLf synthesis. Then we devise three different solution techniques: one based on direct automata manipulation, which is 2EXPTIME, one disregarding unreliable input variables by adopting a belief construction, which is 3EXPTIME, and one leveraging second-order quantified LTLf (QLTLf), which is 2EXPTIME and allows for a direct encoding into monadic second-order logic, which in turn is worst-case nonelementary. We prove their correctness and evaluate them against each other empirically. Interestingly, theoretical worst-case bounds do not translate into observed performance; the MSO technique performs best, followed by belief construction and direct automata manipulation. As a byproduct of our study, we provide a general synthesis procedure for arbitrary QLTLf specifications.

IJCAI Conference 2025 Conference Paper

LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces

• Benjamin Aminof
• Giuseppe De Giacomo
• Sasha Rubin
• Moshe Y. Vardi

We study two logics, LTLf+ and PPLTL+, to express properties of infinite traces, that are based on the linear-time temporal logics LTLf and PPLTL on finite traces. LTLf+/PPLTL+ use levels of Manna and Pnueli’s LTL safety-progress hierarchy, and thus have the same expressive power as LTL. However, they also retain a crucial characteristic of reactive synthesis for the base logics: the game arena for strategy extraction can be derived from deterministic finite automata (DFA). Consequently, these logics circumvent the notorious difficulties associated with determinizing infinite trace automata, typical of LTL synthesis. We present optimal DFA-based technique for solving reactive synthesis for LTLf+ and PPLTL+. Additionally, we adapt these algorithms to optimally solve satisfiability and model-checking for these two logics.

NeSy Conference 2025 Conference Paper

Understanding Boolean Function Learnability on Deep Neural Networks: PAC Learning Meets Neurosymbolic Models

• Márcio Nicolau
• Anderson R. Tavares
• Zhiwei Zhang 0001
• Pedro H. C. Avelar
• João Marcos Flach
• Luís C. Lamb
• Moshe Y. Vardi

Computational learning theory states that many classes of boolean formulas are learnable in polynomial time. This paper addresses the understudied subject of how, in practice, such formulas can be learned by deep neural networks. Specifically, we analyze boolean formulas associated with model-sampling benchmarks, combinatorial optimization problems, and random 3-CNFs with varying degrees of constrainedness. Our experiments indicate that: (i) neural learning generalizes better than pure rule-based systems and pure symbolic approach; (ii) relatively small and shallow neural networks are very good approximators of formulas associated with combinatorial optimization problems; (iii) smaller formulas seem harder to learn, possibly due to the fewer positive (satisfying) examples available; and (iv) interestingly, underconstrained 3-CNF formulas are more challenging to learn than overconstrained ones. Such findings pave the way for a better understanding, construction, and use of neurosymbolic AI methods.

ICRA Conference 2024 Conference Paper

Accelerating Long-Horizon Planning with Affordance-Directed Dynamic Grounding of Abstract Strategies

• Khen Elimelech
• Zachary Kingston
• Wil Thomason
• Moshe Y. Vardi
• Lydia E. Kavraki

Long-horizon task planning is important for robot autonomy, especially as a subroutine for frameworks such as Integrated Task and Motion Planning. However, task planning is computationally challenging and struggles to scale to realistic problem settings. We propose to accelerate task planning over an agent’s lifetime by integrating abstract strategies: a generalizable planning experience encoding introduced in earlier work. In this work, we contribute a practical approach to planning with strategies by introducing a novel formalism of planning in a strategy-augmented domain. We also introduce and formulate the notion of a strategy’s affordance, which indicates its predicted benefit to the solution, and use it to guide the planning and strategy grounding processes. Together, our observations yield an affordance-directed, lazy-search planning algorithm, which can seamlessly compose strategies and actions to solve long-horizon planning problems. We evaluate our planner in an object rearrangement domain, where we demonstrate performance benefits relative to a state-of-the-art task planner.

SAT Conference 2024 Conference Paper

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

• Moshe Y. Vardi

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.

CSL Conference 2024 Conference Paper

Logical Algorithmics: From Theory to Practice (Invited Talk)

• Moshe Y. Vardi

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.

KR Conference 2024 Conference Paper

Probabilistic Synthesis and Verification for LTL on Finite Traces

• Benjamin Aminof
• Linus Cooper
• Sasha Rubin
• Moshe Y. Vardi
• Florian Zuleger

We study synthesis and verification of probabilistic models and specifications over finite traces. Probabilistic models are formalized in this work as Markov Chains and Markov Decisions Processes. Motivated by the recent attention given to, and importance of, finite-trace specifications in AI, we use linear-temporal logic on finite traces as a specification formalism for properties of traces with finite but unbounded time horizons. Since there is no bound on the time horizon, our Markov chains generate infinite traces, and we consider two possible semantics: “existential (resp. universal) prefix- semantics” which says that the finite-trace property holds on some (resp. every) finite prefix of the trace. For both types of semantics, we study two computational problems: the verification problem — “does a given Markov chain satisfy the specification with probability one? ”; and the synthesis problem — “find a strategy (if there is one) that ensures the Markov decision process satisfies the specification with probability one”. We provide optimal algorithms that follow an automata-theoretic approach, and prove that the complexity of the synthesis problem is 2EXPTIME-complete for both semantics, and that for the verification problem it is PSPACE-complete for the universal-prefix semantics, but EXPSPACE-complete for the existential-prefix semantics.

TCS Journal 2024 Journal Article

Singly exponential translation of alternating weak Büchi automata to unambiguous Büchi automata

• Yong Li
• Sven Schewe
• Moshe Y. Vardi

ICRA Conference 2024 Conference Paper

Stochastic Games for Interactive Manipulation Domains

• Karan Muvvala
• Andrew M. Wells
• Morteza Lahijanian
• Lydia E. Kavraki
• Moshe Y. Vardi

As robots become more prevalent, the complexity of robot-robot, robot-human, and robot-environment interactions increases. In these interactions, a robot needs to consider not only the effects of its own actions, but also the effects of other agents’ actions and the possible interactions between agents. Previous works have considered reactive synthesis, where the human/environment is modeled as a deterministic, adversarial agent; as well as probabilistic synthesis, where the human/environment is modeled via a Markov chain. While they provide strong theoretical frameworks, there are still many aspects of human-robot interaction that cannot be fully expressed and many assumptions that must be made in each model. In this work, we propose stochastic games as a general model for human-robot interaction, which subsumes the expressivity of all previous representations. In addition, it allows us to make fewer modeling assumptions and leads to more natural and powerful models of interaction. We introduce the semantics of this abstraction and show how existing tools can be utilized to synthesize strategies to achieve complex tasks with guarantees. Further, we discuss the current computational limitations and improve the scalability by two orders of magnitude by a new way of constructing models for PRISM-games.

ICRA Conference 2023 Conference Paper

Extracting generalizable skills from a single plan execution using abstraction-critical state detection

• Khen Elimelech
• Lydia E. Kavraki
• Moshe Y. Vardi

Robotic task planning is computationally challenging. To reduce planning cost and support life-long operation, we must leverage prior planning experience. To this end, we address the problem of extracting reusable and generalizable abstract skills from successful plan executions. In previous work, we introduced a supporting framework, allowing us, theoretically, to extract an abstract skill from a single execution and later automatically adapt it and reuse it in new domains. We also proved that, given a library of such skills, we can significantly reduce the planning effort for new problems. Nevertheless, until now, abstract-skill extraction could only be performed manually. In this paper, we finally close the automation loop and explain how abstract skills can be practically and automatically extracted. We start by analyzing the desired qualities of an abstract skill and formulate skill extraction as an optimization problem. We then develop two extraction algorithms, based on the novel concept of abstraction-critical state detection. As we show experimentally, the approach is independent of any planning domain.

IJCAI Conference 2023 Conference Paper

Multi-Agent Systems with Quantitative Satisficing Goals

• Senthil Rajasekaran
• Suguman Bansal
• Moshe Y. Vardi

In the study of reactive systems, qualitative properties are usually easier to model and analyze than quantitative properties. This is especially true in systems where mutually beneficial cooperation between agents is possible, such as multi-agent systems. The large number of possible payoffs available to agents in reactive systems with quantitative properties means that there are many scenarios in which agents deviate from mutually beneficial outcomes in order to gain negligible payoff improvements. This behavior often leads to less desirable outcomes for all agents involved. For this reason we study satisficing goals, derived from a decision-making approach aimed at meeting a good-enough outcome instead of pure optimization. By considering satisficing goals, we are able to employ efficient automata-based algorithms to find pure-strategy Nash equilibria. We then show that these algorithms extend to scenarios in which agents have multiple thresholds, providing an approximation of optimization while still retaining the possibility of mutually beneficial cooperation and efficient automata-based algorithms. Finally, we demonstrate a one-way correspondence between the existence of epsilon-equilibria and the existence of equilibria in games where agents have multiple thresholds.

IJCAI Conference 2023 Conference Paper

Solving Quantum-Inspired Perfect Matching Problems via Tutte-Theorem-Based Hybrid Boolean Constraints

• Moshe Y. Vardi
• Zhiwei Zhang

Determining the satisfiability of Boolean constraint-satisfaction problems with different types of constraints, that is hybrid constraints, is a well-studied problem with important applications. We study a new application of hybrid Boolean constraints, which arises in quantum computing. The problem relates to constrained perfect matching in edge-colored graphs. While general-purpose hybrid constraint solvers can be powerful, we show that direct encodings of the constrained-matching problem as hybrid constraints scale poorly and special techniques are still needed. We propose a novel encoding based on Tutte's Theorem in graph theory as well as optimization techniques. Empirical results demonstrate that our encoding, in suitable languages with advanced SAT solvers, scales significantly better than a number of competing approaches on constrained-matching benchmarks. Our study identifies the necessity of designing problem-specific encodings when applying powerful general-purpose constraint solvers.

AAAI Conference 2022 Conference Paper

Constraint-Driven Explanations for Black-Box ML Models

• Aditya A. Shrotri
• Nina Narodytska
• Alexey Ignatiev
• Kuldeep S Meel
• Joao Marques-Silva
• Moshe Y. Vardi

The need to understand the inner workings of opaque Machine Learning models has prompted researchers to devise various types of post-hoc explanations. A large class of such explainers proceed in two phases: first perturb an input instance whose explanation is sought, and then generate an interpretable artifact to explain the prediction of the opaque model on that instance. Recently, Deutch and Frost proposed to use an additional input from the user: a set of constraints over the input space to guide the perturbation phase. While this approach affords the user the ability to tailor the explanation to their needs, striking a balance between flexibility, theoretical rigor and computational cost has remained an open challenge. We propose a novel constraint-driven explanation generation approach which simultaneously addresses these issues in a modular fashion. Our framework supports the use of expressive Boolean constraints giving the user more flexibility to specify the subspace to generate perturbations from. Leveraging advances in Formal Methods, we can theoretically guarantee strict adherence of the samples to the desired distribution. This also allows us to compute fidelity in a rigorous way, while scaling much better in practice. Our empirical study demonstrates concrete uses of our tool CLIME in obtaining more meaningful explanations with high fidelity.

IJCAI Conference 2022 Conference Paper

DPSampler: Exact Weighted Sampling Using Dynamic Programming

• Jeffrey M. Dudek
• Aditya A. Shrotri
• Moshe Y. Vardi

The problem of exact weighted sampling of solutions of Boolean formulas has applications in Bayesian inference, testing, and verification. The state-of-the-art approach to sampling involves carefully decomposing the input formula and compiling a data structure called d-DNNF in the process. Recent work in the closely connected field of model counting, however, has shown that smartly composing different subformulas using dynamic programming and Algebraic Decision Diagrams (ADDs) can outperform d-DNNF-style approaches on many benchmarks. In this work, we present a modular algorithm called DPSampler that extends such dynamic-programming techniques to the problem of exact weighted sampling. DPSampler operates in three phases. First, an execution plan in the form of a project-join tree is computed using tree decompositions. Second, the plan is used to compile the input formula into a succinct tree-of-ADDs representation. Third, this tree is traversed to generate a random sample. This decoupling of planning, compilation and sampling phases enables usage of specialized libraries for each purpose in a black-box fashion. Further, our novel ADD-sampling algorithm avoids the need for expensive dynamic memory allocation required in previous work. Extensive experiments over diverse sets of benchmarks show DPSampler is more scalable and versatile than existing approaches.

TIME Conference 2022 Conference Paper

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

• Moshe Y. Vardi

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.

IJCAI Conference 2022 Conference Paper

LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work

• Giuseppe De Giacomo
• Marco Favorito
• Jianwen Li
• Moshe Y. Vardi
• Shengping Xiao
• Shufang Zhu

Synthesis techniques for temporal logic specifications are typically based on exploiting symbolic techniques, as done in model checking. These symbolic techniques typically use backward fixpoint computation. Planning, which can be seen as a specific form of synthesis, is a witness of the success of forward search approaches. In this paper, we develop a forward-search approach to full-fledged Linear Temporal Logic on finite traces (LTLf) synthesis. We show how to compute the Deterministic Finite Automaton (DFA) of an LTLf formula on-the-fly, while performing an adversarial forward search towards the final states, by considering the DFA as a sort of AND-OR graph. Our approach is characterized by branching on suitable propositional formulas, instead of individual evaluations, hence radically reducing the branching factor of the search space. Specifically, we take advantage of techniques developed for knowledge compilation, such as Sentential Decision Diagrams (SDDs), to implement the approach efficiently.

AAAI Conference 2022 Conference Paper

Synthesis from Satisficing and Temporal Goals

• Suguman Bansal
• Lydia Kavraki
• Moshe Y. Vardi
• Andrew Wells

Reactive synthesis from high-level specifications that combine hard constraints expressed in Linear Temporal Logic (LTL) with soft constraints expressed by discounted-sum (DS) rewards has applications in planning and reinforcement learning. An existing approach combines techniques from LTL synthesis with optimization for the DS rewards but has failed to yield a sound algorithm. An alternative approach combining LTL synthesis with satisficing DS rewards (rewards that achieve a threshold) is sound and complete for integer discount factors, but, in practice, a fractional discount factor is desired. This work extends the existing satisficing approach, presenting the first sound algorithm for synthesis from LTL and DS rewards with fractional discount factors. The utility of our algorithm is demonstrated on robotic planning domains.

KR Conference 2022 Conference Paper

Verification and Realizability in Finite-Horizon Multiagent Systems

• Senthil Rajasekaran
• Moshe Y. Vardi

The problems of verification and realizability are two central themes in the analysis of reactive systems. When multiagent systems are considered, these problems have natural analogues of existence (nonemptiness) of pure-strategy Nash equilibria and verification of pure-strategy Nash equilibria. Recently, this body of work has begun to include finite-horizon temporal goals. With finite-horizon temporal goals, there is a natural hierarchy of goal representation, ranging from deterministic finite automata (DFA), to nondeterministic finite automata (NFA), and to alternating finite automata (AFA), with a worst-case exponential gap between each successive representation. Previous works showed that the realizability problem with DFA goals was PSPACE-complete, while the realizability problem with temporal logic goals is in 2EXPTIME. In this work, we study both the realizability and the verification problems with respect to various goal representations. We first show that the realizability problem with NFA goals is EXPTIME-complete and with AFA goals is 2EXPTIME-complete, thus establishing strict complexity gaps between realizability with respect to DFA, NFA, and AFA goals. We then contrast these complexity gaps with the complexity of the verification problem, where we show that verification with respect to DFAs, NFA, and AFA goals is PSPACE-complete.

ICRA Conference 2021 Conference Paper

Finite-Horizon Synthesis for Probabilistic Manipulation Domains

• Andrew M. Wells
• Zachary Kingston
• Morteza Lahijanian
• Lydia E. Kavraki
• Moshe Y. Vardi

Robots have begun operating and collaborating with humans in industrial and social settings. This collaboration introduces challenges: the robot must plan while taking the human’s actions into account. In prior work, the problem was posed as a 2-player deterministic game, with a limited number of human moves. The limit on human moves is unintuitive, and in many settings determinism is undesirable. In this paper, we present a novel planning method for collaborative human-robot manipulation tasks via probabilistic synthesis. We introduce a probabilistic manipulation domain that captures the interaction by allowing for both robot and human actions with states that represent the configurations of the objects in the workspace. The task is specified using Linear Temporal Logic over finite traces (LTL f ). We then transform our manipulation domain into a Markov Decision Process (MDP) and synthesize an optimal policy to satisfy the specification on this MDP. We present two novel contributions: a formalization of probabilistic manipulation domains allowing us to apply existing techniques and a comparison of different encodings of these domains. Our framework is validated on a physical UR5 robot.

AAMAS Conference 2021 Conference Paper

Nash Equilibria in Finite-Horizon Multiagent Concurrent Games

• Senthil Rajasekaran
• Moshe Y. Vardi

The problem of finding pure strategy Nash equilibria in multiagent concurrent games with finite-horizon temporal goals has received some recent attention. Earlier work solved this problem through the use of Rabin automata. In this work, we take advantage of the finite-horizon nature of the agents’ goals and show that checking for and finding pure strategy Nash equilibria can be done using a combination of safety games and lasso testing in Büchi automata. To separate strategic reasoning from temporal reasoning, we model agents’ goals by deterministic finite-word automata (DFAs), since finite-horizon logics such as LTLf and LDLf are reasoned about through conversion to equivalent DFAs. This allow us characterize the complexity of the problem as PSPACE complete.

GandALF Workshop 2021 Workshop Paper

On the Power of Automata Minimization in Reactive Synthesis

• Shufang Zhu
• Lucas M. Tabajara
• Geguang Pu
• Moshe Y. Vardi

Temporal logic is often used to describe temporal properties in AI applications. The most popular language for doing so is Linear Temporal Logic (LTL). Recently, LTL on finite traces, LTLf, has been investigated in several contexts. In order to reason about LTLf, formulas are typically compiled into deterministic finite automata (DFA), as the intermediate semantic representation. Moreover, due to the fact that DFAs have canonical representation, efficient minimization algorithms can be applied to maximally reduce DFA size, helping to speed up subsequent computations. Here, we present a thorough investigation on two classical minimization algorithms, namely, the Hopcroft and Brzozowski algorithms. More specifically, we show how to apply these algorithms to semi-symbolic (explicit states, symbolic transition functions) automata representation. We then compare the two algorithms in the context of an LTLf-synthesis framework, starting from LTLf formulas. While earlier studies on comparing the two algorithms starting from randomly-generated automata concluded that neither algorithm dominates, our results suggest that starting from LTLf formulas, Hopcroft's algorithm is the best choice in the context of reactive synthesis. Deeper analysis explains why the supposed advantage of Brzozowski's algorithm does not materialize in practice.

SAT Conference 2021 Conference Paper

ProCount: Weighted Projected Model Counting with Graded Project-Join Trees

• Jeffrey M. Dudek
• Vu H. N. Phan
• Moshe Y. Vardi

Abstract Recent work in weighted model counting proposed a unifying framework for dynamic-programming algorithms. The core of this framework is a project-join tree: an execution plan that specifies how Boolean variables are eliminated. We adapt this framework to compute exact literal-weighted projected model counts of propositional formulas in conjunctive normal form. Our key conceptual contribution is to define gradedness on project-join trees, a novel condition requiring irrelevant variables to be eliminated before relevant variables. We prove that building graded project-join trees can be reduced to building standard project-join trees and that graded project-join trees can be used to compute projected model counts. The resulting tool ProCount is competitive with the state-of-the-art tools \(\texttt {D4}_{\texttt {P}}\), projMC, and reSSAT, achieving the shortest solving time on 131 benchmarks of 390 benchmarks solved by at least one tool, from 849 benchmarks in total.

AIJ Journal 2021 Journal Article

Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions

• Anastasios Kyrillidis
• Anshumali Shrivastava
• Moshe Y. Vardi
• Zhiwei Zhang

IJCAI Conference 2021 Conference Paper

Synthesizing Good-Enough Strategies for LTLf Specifications

• Yong Li
• Andrea Turrini
• Moshe Y. Vardi
• Lijun Zhang

We consider the problem of synthesizing good-enough (GE)-strategies for linear temporal logic (LTL) over finite traces or LTLf for short. The problem of synthesizing GE-strategies for an LTL formula φ over infinite traces reduces to the problem of synthesizing winning strategies for the formula (∃Oφ)⇒φ where O is the set of propositions controlled by the system. We first prove that this reduction does not work for LTLf formulas. Then we show how to synthesize GE-strategies for LTLf formulas via the Good-Enough (GE)-synthesis of LTL formulas. Unfortunately, this requires to construct deterministic parity automata on infinite words, which is computationally expensive. We then show how to synthesize GE-strategies for LTLf formulas by a reduction to solving games played on deterministic Büchi automata, based on an easier construction of deterministic automata on finite words. We show empirically that our specialized synthesis algorithm for GE-strategies outperforms the algorithms going through GE-synthesis of LTL formulas by orders of magnitude.

IJCAI Conference 2020 Conference Paper

Graph Neural Networks Meet Neural-Symbolic Computing: A Survey and Perspective

• Luís C. Lamb
• Artur d’Avila Garcez
• Marco Gori
• Marcelo O. R. Prates
• Pedro H. C. Avelar
• Moshe Y. Vardi

Neural-symbolic computing has now become the subject of interest of both academic and industry research laboratories. Graph Neural Networks (GNNs) have been widely used in relational and symbolic domains, with widespread application of GNNs in combinatorial optimization, constraint satisfaction, relational reasoning and other scientific domains. The need for improved explainability, interpretability and trust of AI systems in general demands principled methodologies, as suggested by neural-symbolic computing. In this paper, we review the state-of-the-art on the use of GNNs as a model of neural-symbolic computing. This includes the application of GNNs in several domains as well as their relationship to current developments in neural-symbolic computing.

GandALF Workshop 2020 Workshop Paper

LTLf Synthesis on Probabilistic Systems

• Andrew M. Wells
• Morteza Lahijanian
• Lydia E. Kavraki
• Moshe Y. Vardi

Many systems are naturally modeled as Markov Decision Processes (MDPs), combining probabilities and strategic actions. Given a model of a system as an MDP and some logical specification of system behavior, the goal of synthesis is to find a policy that maximizes the probability of achieving this behavior. A popular choice for defining behaviors is Linear Temporal Logic (LTL). Policy synthesis on MDPs for properties specified in LTL has been well studied. LTL, however, is defined over infinite traces, while many properties of interest are inherently finite. Linear Temporal Logic over finite traces (LTLf) has been used to express such properties, but no tools exist to solve policy synthesis for MDP behaviors given finite-trace properties. We present two algorithms for solving this synthesis problem: the first via reduction of LTLf to LTL and the second using native tools for LTLf. We compare the scalability of these two approaches for synthesis and show that the native approach offers better scalability compared to existing automaton generation tools for LTL.

GandALF Workshop 2020 Workshop Paper

LTLf Synthesis under Partial Observability: From Theory to Practice

• Lucas M. Tabajara
• Moshe Y. Vardi

LTL synthesis is the problem of synthesizing a reactive system from a formal specification in Linear Temporal Logic. The extension of allowing for partial observability, where the system does not have direct access to all relevant information about the environment, allows generalizing this problem to a wider set of real-world applications, but the difficulty of implementing such an extension in practice means that it has remained in the realm of theory. Recently, it has been demonstrated that restricting LTL synthesis to systems with finite executions by using LTL with finite-horizon semantics (LTLf) allows for significantly simpler implementations in practice. With the conceptual simplicity of LTLf, it becomes possible to explore extensions such as partial observability in practice for the first time. Previous work has analyzed the problem of LTLf synthesis under partial observability theoretically and suggested two possible algorithms, one with 3EXPTIME and another with 2EXPTIME complexity. In this work, we first prove a complexity lower bound conjectured in earlier work. Then, we complement the theoretical analysis by showing how the two algorithms can be integrated in practice into an established framework for LTLf synthesis. We furthermore identify a third, MSO-based, approach enabled by this framework. Our experimental evaluation reveals very different results from what the theory seems to suggest, with the 3EXPTIME algorithm often outperforming the 2EXPTIME approach. Furthermore, as long as it is able to overcome an initial memory bottleneck, the MSO-based approach can often outperforms the others.

AAAI Conference 2020 Conference Paper

LTLƒ Synthesis with Fairness and Stability Assumptions

• Shufang Zhu
• Giuseppe De Giacomo
• Geguang Pu
• Moshe Y. Vardi

In synthesis, assumptions are constraints on the environment that rule out certain environment behaviors. A key observation here is that even if we consider systems with LTLf goals on finite traces, environment assumptions need to be expressed over infinite traces, since accomplishing the agent goals may require an unbounded number of environment action. To solve synthesis with respect to finite-trace LTLf goals under infinite-trace assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLf and in LTL have the same worst-case complexity (both 2EXPTIME-complete), the algorithms available for LTL synthesis are much more difficult in practice than those for LTLf synthesis. In this work we show that in interesting cases we can avoid such a detour to LTL synthesis and keep the simplicity of LTLf synthesis. Specifically, we develop a BDD-based fixpoint-based technique for handling basic forms of fairness and of stability assumptions. We show, empirically, that this technique performs much better than standard LTL synthesis.

GandALF Workshop 2020 Workshop Paper

On the Power of Unambiguity in Büchi Complementation

• Yong Li
• Moshe Y. Vardi
• Lijun Zhang

In this work, we exploit the power of unambiguity for the complementation problem of Büchi automata by utilizing reduced run directed acyclic graphs (DAGs) over infinite words, in which each vertex has at most one predecessor. We then show how to use this type of reduced run DAGs as a unified tool to optimize both rank-based and slice-based complementation constructions for Büchi automata with a finite degree of ambiguity. As a result, given a Büchi automaton with n states and a finite degree of ambiguity, the number of states in the complementary Büchi automaton constructed by the classical rank-based and slice-based complementation constructions can be improved, respectively, to 2^O(n) from 2^O(nlogn) and to O(4^n) from O((3n)^n).

AIJ Journal 2020 Journal Article

SAT-based explicit LTL f satisfiability checking

• Jianwen Li
• Geguang Pu
• Yueling Zhang
• Moshe Y. Vardi
• Kristin Y. Rozier

KR Conference 2020 Conference Paper

Two-Stage Technique for LTLf Synthesis Under LTL Assumptions

• Giuseppe De Giacomo
• Antonio Di Stasio
• Moshe Y. Vardi
• Shufang Zhu

In synthesis, assumption are constraints on the environments that rule out certain environment behaviors. A key observation is that even if we consider system with LTLf goals on finite traces, assumptions need to be expressed considering infinite traces, using LTL on infinite traces, since the decision to stop the trace is controlled by the agent. To solve synthesis of LTLf goals under LTL assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTLf and in LTL have the same worst-case complexity (both are 2EXPTIME-complete), the algorithms available for LTL synthesis are much harder in practice than those for LTLf synthesis. Recently, it has been shown that in basic forms of fairness and stability assumptions we can avoid such a detour to LTL and keep the simplicity of LTLf synthesis. In this paper, we generalize these results and show how to effectively handle any kind of LTL assumptions. Specifically, we devise a two-stage technique for solving LTLf under general LTL assumptions and show empirically that this technique performs much better than standard LTL synthesis.

ICRA Conference 2019 Conference Paper

Efficient Symbolic Reactive Synthesis for Finite-Horizon Tasks

• Keliang He
• Andrew M. Wells
• Lydia E. Kavraki
• Moshe Y. Vardi

When humans and robots perform complex tasks together, the robot must have a strategy to choose its actions based on observed human behavior. One well-studied approach for finding such strategies is reactive synthesis. Existing approaches for finite-horizon tasks have used an explicit state approach, which incurs high runtime. In this work, we present a compositional approach to perform synthesis for finite-horizon tasks based on binary decision diagrams. We show that for pick-and-place tasks, the compositional approach achieves orders-of-magnitude speed-ups compared to previous approaches. We demonstrate the synthesized strategy on a UR5 robot.

AAAI Conference 2019 Conference Paper

Learning to Solve NP-Complete Problems: A Graph Neural Network for Decision TSP

• Marcelo Prates
• Pedro H. C. Avelar
• Henrique Lemos
• Luis C. Lamb
• Moshe Y. Vardi

Graph Neural Networks (GNN) are a promising technique for bridging differential programming and combinatorial domains. GNNs employ trainable modules which can be assembled in different configurations that reflect the relational structure of each problem instance. In this paper, we show that GNNs can learn to solve, with very little supervision, the decision variant of the Traveling Salesperson Problem (TSP), a highly relevant NP-Complete problem. Our model is trained to function as an effective message-passing algorithm in which edges (embedded with their weights) communicate with vertices for a number of iterations after which the model is asked to decide whether a route with cost < C exists. We show that such a network can be trained with sets of dual examples: given the optimal tour cost C∗, we produce one decision instance with target cost x% smaller and one with target cost x% larger than C∗. We were able to obtain 80% accuracy training with −2%, +2% deviations, and the same trained model can generalize for more relaxed deviations with increasing performance. We also show that the model is capable of generalizing for larger problem sizes. Finally, we provide a method for predicting the optimal route cost within 2% deviation from the ground truth. In summary, our work shows that Graph Neural Networks are powerful enough to solve NP-Complete problems which combine symbolic and numeric data.

IJCAI Conference 2019 Conference Paper

Not All FPRASs are Equal: Demystifying FPRASs for DNF-Counting (Extended Abstract)

• Kuldeep S. Meel
• Aditya A. Shrotri
• Moshe Y. Vardi

The problem of counting the number of solutions of a DNF formula, also called #DNF, is a fundamental problem in AI with wide-ranging applications. Owing to the intractability of the exact variant, efforts have focused on the design of approximate techniques. Consequently, several Fully Polynomial Randomized Approximation Schemes (FPRASs) based on Monte Carlo techniques have been proposed. Recently, it was discovered that hashing-based techniques too lend themselves to FPRASs for #DNF. Despite significant improvements, the complexity of the hashing-based FPRAS is still worse than that of the best Monte Carlo FPRAS by polylog factors. Two questions were left unanswered in previous works: Can the complexity of the hashing-based techniques be improved? How do these approaches compare empirically? In this paper, we first propose a new search procedure for the hashing-based FPRAS that removes the polylog factors from its time complexity. We then present the first empirical study of runtime behavior of different FPRASs for #DNF, which produces a nuanced picture. We observe that there is no single best algorithm for all formulas and that the algorithm with one of the worst time complexities solves the largest number of benchmarks.

AAAI Conference 2019 Conference Paper

On the Hardness of Probabilistic Inference Relaxations

• Supratik Chakraborty
• Kuldeep S. Meel
• Moshe Y. Vardi

A promising approach to probabilistic inference that has attracted recent attention exploits its reduction to a set of model counting queries. Since probabilistic inference and model counting are #P-hard, various relaxations are used in practice, with the hope that these relaxations allow efficient computation while also providing rigorous approximation guarantees. In this paper, we show that contrary to common belief, several relaxations used for model counting and its applications (including probablistic inference) do not really lead to computational efficiency in a complexity theoretic sense. Our arguments proceed by showing the corresponding relaxed notions of counting to be computationally hard. We argue that approximate counting with multiplicative tolerance and probabilistic guarantees of correctness is the only class of relaxations that provably simplifies the problem, given access to an NP-oracle. Finally, we show that for applications that compare probability estimates with a threshold, a new notion of relaxation with gaps between low and high thresholds can be used. This new relaxation allows efficient decision making in practice, given access to an NP-oracle, while also bounding the approximation error.

IJCAI Conference 2019 Conference Paper

Partitioning Techniques in LTLf Synthesis

• Lucas Martinelli Tabajara
• Moshe Y. Vardi

Decomposition is a general principle in computational thinking, aiming at decomposing a problem instance into easier subproblems. Indeed, decomposing a transition system into a partitioned transition relation was critical to scaling BDD-based model checking to large state spaces. Since then, it has become a standard technique for dealing with related problems, such as Boolean synthesis. More recently, partitioning has begun to be explored in the synthesis of reactive systems. LTLf synthesis, a finite-horizon version of reactive synthesis with applications in areas such as robotics, seems like a promising candidate for partitioning techniques. After all, the state of the art is based on a BDD-based symbolic algorithm similar to those from model checking, and partitioning could be a potential solution to the current bottleneck of this approach, which is the construction of the state space. In this work, however, we expose fundamental limitations of partitioning that hinder its effective application to symbolic LTLf synthesis. We not only provide evidence for this fact through an extensive experimental evaluation, but also perform an in-depth analysis to identify the reason for these results. We trace the issue to an overall increase in the size of the explored state space, caused by an inability of partitioning to fully exploit state-space minimization, which has a crucial effect on performance. We conclude that more specialized decomposition techniques are needed for LTLf synthesis which take into account the effects of minimization.

AAAI Conference 2019 Conference Paper

SAT-Based Explicit LTLf Satisfiability Checking

• Jianwen Li
• Kristin Y. Rozier
• Geguang Pu
• Yueling Zhang
• Moshe Y. Vardi

We present a SAT-based framework for LTLf (Linear Temporal Logic on Finite Traces) satisfiability checking. We use propositional SAT-solving techniques to construct a transition system for the input LTLf formula; satisfiability checking is then reduced to a path-search problem over this transition system. Furthermore, we introduce CDLSC (Conflict-Driven LTLf Satisfiability Checking), a novel algorithm that leverages information produced by propositional SAT solvers from both satisfiability and unsatisfiability results. Experimental evaluations show that CDLSC outperforms all other existing approaches for LTLf satisfiability checking, by demonstrating an approximate four-fold speed-up compared to the second-best solver.

AAAI Conference 2019 Conference Paper

Unbounded Orchestrations of Transducers for Manufacturing

• Natasha Alechina
• Tomáš Brázdil
• Giuseppe De Giacomo
• Paolo Felli
• Brian Logan
• Moshe Y. Vardi

There has recently been increasing interest in using reactive synthesis techniques to automate the production of manufacturing process plans. Previous work has assumed that the set of manufacturing resources is known and fixed in advance. In this paper, we consider the more general problem of whether a controller can be synthesized given sufficient resources. In the unbounded setting, only the types of available manufacturing resources are given, and we want to know whether it is possible to manufacture a product using only resources of those type(s), and, if so, how many resources of each type are needed. We model manufacturing processes and facilities as transducers (automata with output), and show that the unbounded orchestration problem is decidable and the (Pareto) optimal set of resources necessary to manufacture a product is computable for uni-transducers. However, for multitransducers, the problem is undecidable.

IROS Conference 2017 Conference Paper

Reactive synthesis for finite tasks under resource constraints

• Keliang He
• Morteza Lahijanian
• Lydia E. Kavraki
• Moshe Y. Vardi

There are many applications where robots have to operate in environments that other agents can change. In such cases, it is desirable for the robot to achieve a given high-level task despite interference. Ideally, the robot must decide its next action as it observes the changes in the world, i. e. act reactively. In this paper, we consider a reactive planning problem for finite robotic tasks with resource constraints. The task is represented using a temporal logic for finite behaviors and the robot must achieve the task using limited resources under all possible finite sequences of moves of other agents. We present a formulation for this problem and an approach based on quantitative games. The efficacy of the approach is demonstrated through a manipulation case study.

IJCAI Conference 2017 Conference Paper

Symbolic LTLf Synthesis

• Shufang Zhu
• Lucas M. Tabajara
• Jianwen Li
• Geguang Pu
• Moshe Y. Vardi

LTLf synthesis is the process of finding a strategy that satisfies a linear temporal specification over finite traces. An existing solution to this problem relies on a reduction to a DFA game. In this paper, we propose a symbolic framework for LTLf synthesis based on this technique, by performing the computation over a representation of the DFA as a boolean formula rather than as an explicit graph. This approach enables strategy generation by utilizing the mechanism of boolean synthesis. We implement this symbolic synthesis method in a tool called Syft, and demonstrate by experiments on scalable benchmarks that the symbolic approach scales better than the explicit one.

IJCAI Conference 2017 Conference Paper

The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas

• Jeffrey M. Dudek
• Kuldeep S. Meel
• Moshe Y. Vardi

Recent universal-hashing based approaches to sampling and counting crucially depend on the runtime performance of SAT solvers on formulas expressed as the conjunction of both CNF constraints and variable-width XOR constraints (known as CNF-XOR formulas). In this paper, we present the first study of the runtime behavior of SAT solvers equipped with XOR-reasoning techniques on random CNF-XOR formulas. We empirically demonstrate that a state-of-the-art SAT solver scales exponentially on random CNF-XOR formulas across a wide range of XOR-clause densities, peaking around the empirical phase-transition location. On the theoretical front, we prove that the solution space of a random CNF-XOR formula 'shatters' at all nonzero XOR-clause densities into well-separated components, similar to the behavior seen in random CNF formulas known to be difficult for many SAT algorithms.

IJCAI Conference 2016 Conference Paper

Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls

• Supratik Chakraborty
• Kuldeep S. Meel
• Moshe Y. Vardi

Probabilistic inference via model counting has emerged as a scalable technique with strong formal guarantees, thanks to recent advances in hashing-based approximate counting. State-of-the-art hashing-based counting algorithms use an NP oracle, such that the number of oracle invocations grows linearly in the number of variables n in the input constraint. We present a new approach to hashing-based approximate model counting in which the number of oracle invocations grows logarithmically in n, while still providing strong theoretical guarantees. We use this technique to design an algorithm for #CNF with strongly probably approximately correct (SPAC) guarantees, i. e. PAC guarantee plus expected return value matching the exact model count. Our experiments show that this algorithm outperforms state-of-the-art techniques for approximate counting by 1-2 orders of magnitude in running time. We also show that our algorithm can be easily adapted to give a new fully polynomial randomized approximation scheme (FPRAS) for #DNF.

IJCAI Conference 2015 Conference Paper

From Weighted to Unweighted Model Counting

• Supratik Chakraborty
• Dror Fried
• Kuldeep S. Meel
• Moshe Y. Vardi

The recent surge of interest in reasoning about probabilistic graphical models has led to the development of various techniques for probabilistic reasoning. Of these, techniques based on weighted model counting are particularly interesting since they can potentially leverage recent advances in unweighted model counting and in propositional satisfiability solving. In this paper, we present a new approach to weighted model counting via reduction to unweighted model counting. Our reduction, which is polynomial-time and preserves the normal form (CNF/DNF) of the input formula, allows us to exploit advances in unweighted model counting to solve weighted model counting instances. Experiments with weighted model counters built using our reduction indicate that these counters performs much better than a state-of-the-art weighted model counter.

ICRA Conference 2015 Conference Paper

Towards manipulation planning with temporal logic specifications

• Keliang He
• Morteza Lahijanian
• Lydia E. Kavraki
• Moshe Y. Vardi

Manipulation planning from high-level task specifications, even though highly desirable, is a challenging problem. The large dimensionality of manipulators and complexity of task specifications make the problem computationally intractable. This work introduces a manipulation planning framework with linear temporal logic (LTL) specifications. The use of LTL as the specification language allows the expression of rich and complex manipulation tasks. The framework deals with the state-explosion problem through a novel abstraction technique. Given a robotic system, a workspace consisting of obstacles, manipulable objects, and locations of interest, and a co-safe LTL specification over the objects and locations, the framework computes a motion plan to achieve the task through a synergistic multi-layered planning architecture. The power of the framework is demonstrated through case studies, in which the planner efficiently computes plans for complex tasks. The case studies also illustrate the ability of the framework in intelligently moving away objects that block desired executions without requiring backtracking.

ICRA Conference 2014 Conference Paper

A sampling-based strategy planner for nondeterministic hybrid systems

• Morteza Lahijanian
• Lydia E. Kavraki
• Moshe Y. Vardi

This paper introduces a strategy planner for nondeterministic hybrid systems with complex continuous dynamics. The planner uses sampling-based techniques and game-theoretic approaches to generate a series of plans and decision choices that increase the chances of success within a fixed time budget. The planning algorithm consists of two phases: exploration and strategy improvement. During the exploration phase, a search tree is grown in the hybrid state space by sampling state and control spaces for a fixed amount of time. An initial strategy is then computed over the search tree using a game-theoretic approach. To mitigate the effects of nondeterminism in the initial strategy, the strategy improvement phase extends new tree branches to the goal, using the data that is collected in the first phase. The efficacy of this planner is demonstrated on simulation of two hybrid and nondeterministic car-like robots in various environments. The results show significant increases in the likelihood of success for the strategies computed by the two-phase algorithm over a simple exploration planner.

ECAI Conference 2014 Conference Paper

LTLf Satisfiability Checking

• Jianwen Li
• Lijun Zhang 0001
• Geguang Pu
• Moshe Y. Vardi
• Jifeng He 0001

We consider here Linear Temporal Logic (LTL) formulas interpreted over finite traces. We denote this logic by LTLf. The existing approach for LTLfsatisfiability checking is based on a reduction to standard LTL satisfiability checking. We describe here a novel direct approach to LTLfsatisfiability checking, where we take advantage of the difference in the semantics between LTL and LTLf. While LTL satisfiability checking requires finding a fair cycle in an appropriate transition system, here we need to search only for a finite trace. This enables us to introduce specialized heuristics, where we also exploit recent progress in Boolean SAT solving. We have implemented our approach in a prototype tool and experiments show that our approach outperforms existing approaches.

EUMAS Conference 2014 Conference Paper

Synthesis with Rational Environments

• Orna Kupferman
• Giuseppe Perelli
• Moshe Y. Vardi

Abstract Synthesis is the automated construction of a system from its specification. The system has to satisfy its specification in all possible environments. The environment often consists of agents that have objectives of their own. Thus, it makes sense to soften the universal quantification on the behavior of the environment and take the objectives of its underlying agents into an account. Fisman et al. introduced rational synthesis: the problem of synthesis in the context of rational agents. The input to the problem consists of temporal-logic formulas specifying the objectives of the system and the agents that constitute the environment, and a solution concept (e. g. , Nash equilibrium). The output is a profile of strategies, for the system and the agents, such that the objective of the system is satisfied in the computation that is the outcome of the strategies, and the profile is stable according to the solution concept; that is, the agents that constitute the environment have no incentive to deviate from the strategies suggested to them. In this paper we continue to study rational synthesis. First, we suggest an alternative definition to rational synthesis, in which the agents are rational but not cooperative. In the non-cooperative setting, one cannot assume that the agents that constitute the environment take into account the strategies suggested to them. Accordingly, the output is a strategy for the system only, and the objective of the system has to be satisfied in all the compositions that are the outcome of a stable profile in which the system follows this strategy. We show that rational synthesis in this setting is 2 ExpTime - complete, thus it is not more complex than traditional synthesis or cooperative rational synthesis. Second, we study a richer specification formalism, where the objectives of the system and the agents are not Boolean but quantitative. In this setting, the goal of the system and the agents is to maximize their outcome. The quantitative setting significantly extends the scope of rational synthesis, making the game-theoretic approach much more relevant.

Highlights Conference 2013 Conference Abstract

Invited Talk: The rise and fall of Linear Temporal Logic

• Moshe Y. Vardi

One of the surprising developments in the area of program verification in the late part of the 20th Century is the emergence of Linear Temporal Logic (LTL), a logic that emerged in philisophical studies of free will, as the cannonical language for describing temporal behavior of computer systems. LTL, however, is not expressive enough for industrial applications. The first decade of the 21 Century saw the emergence of industrial temporal logics such as ForSpec, PSL, and SVA. These logics, however, are not clean enough to serve as objects of theoretical study. This talk will describe the rise and fall of LTL, and will propose a new cannonical temporal logic: Linear Dynamic Logic (LDL). 09: 50 10: 00 Break

IJCAI Conference 2013 Conference Paper

Linear Temporal Logic and Linear Dynamic Logic on Finite Traces

• Giuseppe De Giacomo
• Moshe Y. Vardi

In this paper we look into the assumption of interpreting LTL over finite traces. In particular we show that LTLf, i. e. , LTL under this assumption, is less expressive than what might appear at first sight, and that at essentially no computational cost one can make a significant increase in expressiveness while maintaining the same intuitiveness of LTLf. Indeed, we propose a logic, LDLf for Linear Dynamic Logic over finite traces, which borrows the syntax from Propositional Dynamic Logic (PDL), but is interpreted over finite traces. Satisfiability, validity and logical implication (as well as model checking) for LDLf are PSPACE-complete as for LTLf (and LTL).

TIME Conference 2013 Conference Paper

LTL Satisfiability Checking Revisited

• Jianwen Li
• Lijun Zhang 0001
• Geguang Pu
• Moshe Y. Vardi
• Jifeng He 0001

We propose a novel algorithm for the satisfiability problem for Linear Temporal Logic (LTL). Existing approaches first transform the LTL formula into a B"uchi automaton and then perform an emptiness checking of the resulting automaton. Instead, our approach works on-the-fly by inspecting the formula directly, thus enabling finding a satisfying model quickly without constructing the full automaton. This makes our algorithm particularly fast for satisfiable formulas. We report on a prototype implementation, showing that our approach significantly outperforms state-of-the-art tools.

GandALF Workshop 2013 Workshop Paper

Profile Trees for Büchi Word Automata, with Application to Determinization

• Seth Fogarty
• Orna Kupferman
• Moshe Y. Vardi
• Thomas Wilke

The determinization of Buchi automata is a celebrated problem, with applications in synthesis, probabilistic verification, and multi-agent systems. Since the 1960s, there has been a steady progress of constructions: by McNaughton, Safra, Piterman, Schewe, and others. Despite the proliferation of solutions, they are all essentially ad-hoc constructions, with little theory behind them other than proofs of correctness. Since Safra, all optimal constructions employ trees as states of the deterministic automaton, and transitions between states are defined operationally over these trees. The operational nature of these constructions complicates understanding, implementing, and reasoning about them, and should be contrasted with complementation, where a solid theory in terms of automata run DAGs underlies modern constructions. In 2010, we described a profile-based approach to Buchi complementation, where a profile is simply the history of visits to accepting states. We developed a structural theory of profiles and used it to describe a complementation construction that is deterministic in the limit. Here we extend the theory of profiles to prove that every run DAG contains a profile tree with at most a finite number of infinite branches. We then show that this property provides a theoretical grounding for a new determinization construction where macrostates are doubly preordered sets of states. In contrast to extant determinization constructions, transitions in the new construction are described declaratively rather than operationally.

Highlights Conference 2013 Conference Abstract

Semantic acyclicity on graph databases

• Pablo Barcelo
• Gaëlle Fontaine
• Miguel Romero
• Moshe Y. Vardi

Unions of acyclic conjunctive queries (CQs) can be evaluated in linear time, as opposed to arbitrary CQs, for which the evaluation problem is NP-complete. It is known that evaluation of semantically acyclic unions of CQs - i. e. , unions of CQs that are equivalent to a union of acyclic ones - is tractable. We study the notion of semantic acyclicity in the context of graph databases and unions of conjunctive regular path queries (UCRPQs). We prove that checking whether a UCRPQ is semantically acyclic is decidable in 2ExpSpace and is ExpSpace-hard. We show that evaluation of semantically acyclic UCRPQs is fixed-parameter tractable.

CSL Conference 2011 Conference Paper

Branching vs. Linear Time: Semantical Perspective

• Moshe Y. Vardi

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.

CSL Conference 2011 Conference Paper

Synthesis from Probabilistic Components

• Yoad Lustig
• Sumit Nain
• Moshe Y. Vardi

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.

CSL Conference 2011 Conference Paper

Unifying Büchi Complementation Constructions

• Seth Fogarty
• Orna Kupferman
• Moshe Y. Vardi
• Thomas Wilke

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.

ICAPS Conference 2010 Invited Paper

From Automated Verification to Automated Design

• Moshe Y. Vardi

In this talk I will review 50 years of research on the design-synthesis problem and show how the automata-theoretic approach can be used to solve it.

ICRA Conference 2010 Conference Paper

Sampling-based motion planning with temporal goals

• Amit Bhatia 0001
• Lydia E. Kavraki
• Moshe Y. Vardi

This paper presents a geometry-based, multi-layered synergistic approach to solve motion planning problems for mobile robots involving temporal goals. The temporal goals are described over subsets of the workspace (called propositions) using temporal logic. A multi-layered synergistic framework has been proposed recently for solving planning problems involving significant discrete structure. In this framework, a high-level planner uses a discrete abstraction of the system and the exploration information to suggest feasible high-level plans. A low-level sampling-based planner uses the physical model of the system, and the suggested high-level plans, to explore the state-space for feasible solutions. In this paper, we advocate the use of geometry within the above framework to solve motion planning problems involving temporal goals. We present a technique to construct the discrete abstraction using the geometry of the obstacles and the propositions defined over the workspace. Furthermore, we show through experiments that the use of geometry results in significant computational speedups compared to previous work. Traces corresponding to trajectories of the system are defined employing the sampling interval used by the low-level algorithm. The applicability of the approach is shown for second-order nonlinear robot models in challenging workspace environments with obstacles, and for a variety of temporal logic specifications.

SAT Conference 2009 Invited Paper

Symbolic Techniques in Propositional Satisfiability Solving

• Moshe Y. Vardi

Abstract Search-based techniques in propositional satisfiability (SAT) solving have been enormously successful, leading to what is becoming known as the “SAT Revolution”. Essentially all state-of-the-art SAT solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) technique, augmented with backjumping and conflict learning. Much of current research in this area involves refinements and extensions of the DPLL technique. Yet, due to the impressive success of DPLL, little effort has gone into investigating alternative techniques. This work focuses on symbolic techniques for SAT solving, with the aim of stimulating a broader research agenda in this area.

ICRA Conference 2008 Conference Paper

Impact of workspace decompositions on discrete search leading continuous exploration (DSLX) motion planning

• Erion Plaku
• Lydia E. Kavraki
• Moshe Y. Vardi

We have recently proposed DSLX, a motion planner that significantly reduces the computational time for solving challenging kinodynamic problems by interleaving continuous state-space exploration with discrete search on a workspace decomposition. An important but inadequately understood aspect of DSLX is the role of the workspace decomposition on the computational efficiency of the planner. Understanding this role is important for successful applications of DSLX to increasingly complex robotic systems. This work shows that the granularity of the workspace decomposition directly impacts computational efficiency: DSLX is faster when the decomposition is neither too fine-nor too coarse-grained. Finding the right level of granularity can require extensive fine-tuning. This work demonstrates that significant computational efficiency can instead be obtained with no fine-tuning by using conforming Delaunay triangulations, which in the context of DSLX provide a natural workspace decomposition that allows an efficient interplay between continuous state-space exploration and discrete search. The results of this work are based on extensive experiments on DSLX using grid, trapezoidal, and triangular decompositions of various granularities to solve challenging first and second-order kinodynamic motion-planning problems.

ICRA Conference 2007 Conference Paper

A Motion Planner for a Hybrid Robotic System with Kinodynamic Constraints

• Erion Plaku
• Lydia E. Kavraki
• Moshe Y. Vardi

The rapidly increasing complexity of tasks robotic systems are expected to carry out underscores the need for the development of motion planners that can take into account discrete changes in the continuous motions of the system. Completion of tasks such as exploration of unknown or hazardous environments often requires discrete changes in the controls and motions of the robot in order to adapt to different terrains or maintain operability during partial failures or other mishaps. The contribution of this work toward this objective is the development of an efficient motion planner for a hybrid robotic system. The controls and motion equations of the robot could change discretely in order to enable the robot to operate in different terrains. The framework in this paper blends discrete searching with sampling-based motion planning for continuous state spaces and is well-suited for robotic systems modeled as hybrid systems with numerous discrete modes and transitions. This multi-layered approach offers considerable improvements over existing methods addressing similar problems, as indicated by the experimental results.

TCS Journal 2007 Journal Article

View-based query processing: On the relationship between rewriting, answering and losslessness

• Diego Calvanese
• Giuseppe De Giacomo
• Maurizio Lenzerini
• Moshe Y. Vardi

LPAR Conference 2006 Conference Paper

On Locally Checkable Properties

• Orna Kupferman
• Yoad Lustig
• Moshe Y. Vardi

Abstract The large computational price of formal verification of general ω -regular properties has led to the study of restricted classes of properties, and to the development of verification methodologies for them. Examples that have been widely accepted by the industry include the verification of safety properties, and bounded model checking. We introduce and study another restricted class of properties – the class of locally checkable properties. For an integer k ≥1, a language L ⊆ Σ ω is k-checkable if there is a language R ⊆ Σ k (of “allowed subwords”) such that a word w belongs to L iff all the subwords of w of length k belong to R. A property is locally checkable if its language is k -checkable for some k. Locally checkable properties, which are a special case of safety properties, are common in the specification of systems. In particular, one can often bound an eventuality constraint in a property by a fixed time frame. The practical importance of locally checkable properties lies in the low memory demand for their run-time verification. A monitor for a k -checkable property needs only a record of the last k computation cycles. Furthermore, even if a large number of k -checkable properties are monitored, the monitors can share their memory, resulting in memory demand that do not depend on the number of properties monitored. This advantage of locally checkable properties makes them particularly suitable for run-time verification. In the paper, we define locally checkable languages, study their relation to other restricted classes of properties, study the question of deciding whether a property is locally checkable, and study the relation between the size of the property (specified by an LTL formula or an automaton) and the smallest k for which the property is k -checkable.

TCS Journal 2005 Journal Article

Decidable containment of recursive queries

• Diego Calvanese
• Giuseppe De Giacomo
• Moshe Y. Vardi

LPAR Conference 2005 Conference Paper

Experimental Evaluation of Classical Automata Constructions

• Deian Tabakov
• Moshe Y. Vardi

Abstract There are several algorithms for producing the canonical DFA from a given NFA. While the theoretical complexities of these algorithms are known, there has not been a systematic empirical comparison between them. In this work we propose a probabilistic framework for testing the performance of automata-theoretic algorithms. We conduct a direct experimental comparison between Hopcroft’s and Brzozowski’s algorithms. We show that while Hopcroft’s algorithm has better overall performance, Brzozowski’s algorithm performs better for “high-density” NFA. We also consider the universality problem, which is traditionally solved explicitly via the subset construction. We propose an encoding that allows this problem to be solved symbolically via a model-checker. We compare the performance of this approach to that of the standard explicit algorithm, and show that the explicit approach performs significantly better.

TCS Journal 2005 Journal Article

From complementation to certification

• Orna Kupferman
• Moshe Y. Vardi

FOCS Conference 2005 Conference Paper

Safraless Decision Procedures

• Orna Kupferman
• Moshe Y. Vardi

The automata-theoretic approach is one of the most fundamental approaches to developing decision procedures in mathematical logics. To decide whether a formula in a logic with the tree-model property is satisfiable, one constructs an automaton that accepts all (or enough) tree models of the formula and then checks that the language of this automaton is nonempty. The standard approach translates formulas into alternating parity tree automata, which are then translated, via Safra's determinization construction, into nondeterministic parity automata. This approach is not amenable to implementation because of the difficulty of implementing Safra's construction and the nonemptiness test for nondeterministic parity tree automata. In this paper, we offer an alternative to the standard automata-theoretic approach. The crux of our approach is avoiding the use of Safra's construction and of nondeterministic parity tree automata. Our approach goes instead via universal co-Buchi tree automata and nondeterministic Buchi tree automata. Our translations are significantly simpler than the standard approach, less difficult to implement, and have practical advantages like being amenable to optimizations and a symbolic implementation. We also show that our approach yields better complexity bounds.

LPAR Conference 2005 Conference Paper

Treewidth in Verification: Local vs. Global

• Andrea Ferrara
• Guoqiang Pan
• Moshe Y. Vardi

Abstract The treewidth of a graph measures how close the graph is to a tree. Many problems that are intractable for general graphs, are tractable when the graph has bounded treewidth. Recent works study the complexity of model checking for state transition systems of bounded treewidth. There is little reason to believe, however, that the treewidth of the state transition graphs of real systems, which we refer to as global treewidth, is bounded. In contrast, we consider in this paper concurrent transition systems, where communication between concurrent components is modeled explicitly. Assuming boundedness of the treewidth of the communication graph, which we refer to as local treewidth, is reasonable, since the topology of communication in concurrent systems is often constrained physically. In this work we study the impact of local treewidth boundedness on the complexity of verification problems. We first present a positive result, proving that a CNF formula of bounded treewidth can be represented by an OBDD of polynomial size. We show, however, that the nice properties of treewidth-bounded CNF formulas are not preserved under existential quantification or unrolling. Finally, we show that the complexity of various verification problems is high even under the assumption of local treewidth boundedness. In summary, while global treewidth boundedness does have computational advantages, it is not a realistic assumption; in contrast, local treewidth boundedness is a realistic assumption, but its computational advantages are rather meager.

SAT Conference 2004 Conference Paper

Search vs. Symbolic Techniques in Satisfiability Solving

• Guoqiang Pan
• Moshe Y. Vardi

Recent work has shown how to use OBDDs for satisfiability solving. The idea of this approach, which we call symbolic quantifier elimination, is to view an instance of propositional satisfiability as an existentially quantified propositional formula. Satisfiability solving then amounts to quantifier elimination; once all quantifiers have been eliminated we are left with either 1 or 0. Our goal in this work is to study the effectiveness of symbolic quantifier elimination as an approach to satisfiability solving. To that end, we conduct a direct comparison with the DPLL-based ZChaff, as well as evaluate a variety of optimization techniques for the symbolic approach. In comparing the symbolic approach to ZChaff, we evaluate scalability across a variety of classes of formulas. We find that no approach dominates across all classes. While ZChaff dominates for many classes of formulas, the symbolic approach is superior for other classes of formulas. Once we have demonstrated the viability of the symbolic approach, we focus on optimization techniques for this approach. We study techniques from constraint satisfaction for finding a good plan for performing the symbolic operations of conjunction and of existential quantification. We also study various variable-ordering heuristics, finding that while no heuristic seems to dominate across all classes of formulas, the maximum-cardinality search heuristic seems to offer the best overall performance.

TCS Journal 2003 Journal Article

From bidirectionality to alternation

• Nir Piterman
• Moshe Y. Vardi

JELIA Conference 2002 Invited Paper

Alternation

• Moshe Y. Vardi

Abstract Alternation was introduced in the late 1970s as a complexitytheoretic construct, capturing the computational aspect of games. Since then it has also been shown that alternation can be viewed as a powerful high level algorithmic construct, which is particularly suitable for automated reasoning. In this talk I will explain how to turn alternation from a complexity-theoretic construct to an algorithmic construct and demonstrate its applicability in the context of modal and temporal reasoning. A particular emphasis will be put on the use of alternating automata as an algorithmic tool.

KR Conference 2002 Conference Paper

Eliminating Incoherence from Subjective Estimates of Chance

• Randy Batsell
• Lyle Brenner
• Daniel Osherson
• Spyros Tsavachidis
• Moshe Y. Vardi

LPAR Conference 2002 Conference Paper

Pushdown Specifications

• Orna Kupferman
• Nir Piterman
• Moshe Y. Vardi

Abstract Traditionally, model checking is applied to finite-state systems and regular specifications. While researchers have successfully extended the applicability of model checking to infinite-state systems, almost all existing work still consider regular specification formalisms. There are, however, many interesting non-regular properties one would like to model check. In this paper we study model checking of pushdown specifications. Our specification formalism is nondeterministic pushdown parity tree automata (PD-NPT). We show that the model-checking problem for regular systems and PD-NPT specifications can be solved in time exponential in the system and the specification. Our model-checking algorithm involves a new solution to the nonemptiness problem of nondeterministic pushdown tree automata, where we improve the best known upper bound from a triple-exponential to a single exponential. We also consider the model-checking problem for context-free systems and PD-NPT specifications and show that it is undecidable.

KR Conference 2002 Conference Paper

Reasoning about Actions and Planning in LTL Action Theories

• Diego Calvanese
• Giuseppe De Giacomo
• Moshe Y. Vardi

MFCS Conference 2001 Conference Paper

From Bidirectionality to Alternation

• Nir Piterman
• Moshe Y. Vardi

Abstract We describe an explicit simulation of 2-way nondeterministic automata by 1-way alternating automata with quadratic blow-up. We first describe the construction for automata on finite words, and extend it to automata on infinite words.

LPAR Conference 2001 Conference Paper

On Bounded Specifications

• Orna Kupferman
• Moshe Y. Vardi

Abstract Bounded model checking methodologies check the correctness of a system with respect to a given specification by examining computations of a bounded length. Results from set-theoretic topology imply that sets in Σ ω that are both open and closed ( clopen sets ) are precisely bounded sets: membership of a word in a clopen set can be determined by examining a bounded prefix of it. Clopen sets correspond to specifications that are both safety and co-safety. In this paper we study bounded specifications from this perspective. We consider both the linear and the branching frameworks. In the linear framework, we show that when clopen specifications are given by word automata or temporal logic formulas, we can identify a bound and translate the specification to bounded formalisms such as cycle-free automata and bounded LTL. In the branching framework, we show that while clopen sets of trees with infinite branching degrees may not be bounded, we can extend the results from the linear framework to clopen specifications given by tree automata or temporal logic formulas, even for trees with infinite branching degrees. There, we can identify a bound and translate clopen specifications to cycle-free automata and modal logic. Finally, we show how our results imply that the bottom levels of the μ-calculus hierarchy coalesce.

MFCS Conference 2000 Invited Paper

0-1 Laws for Fragments of Existential Second-Order Logic: A Survey

• Phokion G. Kolaitis
• Moshe Y. Vardi

Abstract The probability of a property on the collection of all finite relational structures is the limit as n → ∞ of the fraction of structures with n elements satisfying the property, provided the limit exists. It is known that the 0-1 law holds for every property expressible in first-order logic, i. e. , the probability of every such property exists and is either 0 or 1. Moreover, the associated decision problem for the probabilities is solvable. In this survey, we consider fragments of existential second-order logic in which we restrict the patterns of first-order quantifiers. We focus on fragments in which the first-order part belongs to a prefix class. We show that the classifications of prefix classes of first-order logic with equality according to the solvability of the finite satisfiability problem and according to the 0-1 law for the corresponding Σ 1 1 fragments are identical, but the classifications are different without equality.

CSL Conference 2000 Invited Paper

Automated Verification = Graphs, Automata, and Logic

• Moshe Y. Vardi

Abstract In automated verification one uses algorithmic techniques to establish the correctness of the design with respect to a given property. Automated verification is based on a small number of key algorithmic ideas, tying together graph theory, automata theory, and logic. In this self-contained talk I will describe how this “holy trinity” gave rise to automated-verification tools.

MFCS Conference 2000 Conference Paper

µ-Calculus Synthesis

• Orna Kupferman
• Moshe Y. Vardi

Abstract In system synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. When the system is open, it interacts with an environment via input and output signals and its behavior depends on this interaction. An open system should satisfy its specification in all possible environments. In addition to the input signals that the system can read, an environment can also have internal signals that the system cannot read. In the above setting, of synthesis with incomplete information, we should transform a specification that refers to both readable and unreadable signals into a system whose behavior depends only on the readable signals. In this work we solve the problem of synthesis with incomplete information for specifications in μ-calculus. Since many properties of systems are naturally specified by means of fixed points, the μ-calculus is an expressive and important specification language. Our results and technique generalize and simplify previous work on synthesis. In particular, we prove that the problem of μ-calculus synthesis with incomplete information is EXPTIME-complete. Thus, it is not harder than the satisfiability or the synthesis problems for this logic.

TCS Journal 1998 Journal Article

Foreword

• Georg Gottlob
• Moshe Y. Vardi

STOC Conference 1998 Conference Paper

Weak Alternating Automata and Tree Automata Emptiness

• Orna Kupferman
• Moshe Y. Vardi

TARK Conference 1996 Conference Paper

Common Knowledge Revisited

• Ronald Fagin
• Joseph Y. Halpern
• Yoram Moses
• Moshe Y. Vardi

We consider the common-knowledge paradox raised in [HM90]: common knowledge is necessary for coordination, but common knowledge is unattainable in the real world because of temporal imprecision. We discuss two solutions to this paradox: (1) modeling the world with a coarser granularity, and (2) relaxing the requirements for coordination.

TARK Conference 1996 Conference Paper

Implementing Knowledge-Based Programs

• Moshe Y. Vardi

Reasoning about multi-agents systems at the knowledge level allows us to abstract away from many concrete details of the systems we are considering. Fagin et al. introduced two notions to facilitate designing and reasoning about systems in terms of knowledge. The first notion is that of knowledge-based programs. Knowledge-based programs are defined as syntactic objects: programs with tests for knowledge. The second notion is that of contexts, which capture the setting in which a program is to be executed. In a given context, a standard program (one without tests for knowledge) is always implementable. A knowledge-based program, on the other hand, might not be implementable. We provide a condition which is necessary and sufficient to guarantee that a given knowledge-based program is implemented by a given protocol, and we completely characterize the complexity of determining whether a given knowledge-based program is implemented by a given protocol in a given finite-state context. In particular, we identify an important special case where this problem is tractable.

AIJ Journal 1995 Journal Article

A nonstandard approach to the logical omniscience problem

• Ronald Fagin
• Joseph Y. Halpern
• Moshe Y. Vardi

TCS Journal 1995 Journal Article

Computing with infinitary logic

• Serge Abiteboul
• Moshe Y. Vardi
• Victor Vianu

TARK Conference 1994 Conference Paper

Algorithmic Knowledge

• Joseph Y. Halpern
• Yoram Moses
• Moshe Y. Vardi

The standard model of knowledge in multi-agent systems suffers from what has been called the logical omniscience problem: agents know all tautologies, and know all the logical consequences of their knowledge. For many types of analysis, this turns out not to be a problem. Knowledge is viewed as being ascribed by the system designer to the agents; agents are not assumed to compute their knowledge in any way, nor is it assumed that they can necessarily answer questions based on their knowledge. Nevertheless, in many applications that we are interested in, agents need to act on their knowledge. In such applications, an externally ascribed notion of knowledge is insufficient: clearly an agent can base his actions only on what he explicitly knows. Furthermore, an agent that has to act on his knowledge has to be able to compute this knowledge; we do need to take into account the algorithms available to the agent, as well as the "effort" required to compute knowledge. In this paper, we show how the standard model can be modified in a natural way to take the computational aspects of knowledge into account. *Current address: Dept. of Computer Science, Rice University, P. O. Box 1892, Houston, TX 77251-1892,

CSL Conference 1994 Conference Paper

The Complexity of Set Constraints

• Alexander Aiken
• Dexter Kozen
• Moshe Y. Vardi
• Edward L. Wimmers

Abstract Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. We present several results on the computational complexity of solving systems of set constraints. The systems we study form a natural complexity hierarchy depending on the form of the constraint language.

STOC Conference 1993 Conference Paper

Monotone monadic SNP and constraint satisfaction

• Tomás Feder
• Moshe Y. Vardi

TCS Journal 1993 Journal Article

On the complexity of queries in the logical data model

• Gabriel M. Kuper
• Moshe Y. Vardi

STOC Conference 1993 Conference Paper

Parametric real-time reasoning

• Rajeev Alur
• Thomas A. Henzinger
• Moshe Y. Vardi

TARK Conference 1992 Conference Paper

The Expressive Power of the Kierarchical Approach to Modeling Knowledge and Common Knowledge

• Ronald Fagin
• John Geanakoplos
• Joseph Y. Halpern
• Moshe Y. Vardi

One approach to representing knowledge or belief of agents, which has been explored independently by economists (BSge and Eisele; Mertens and Zamir; Brandenburger and Dekel; Tan and Werlang) and by computer scientists (Fagin, Halpern, and Vardi) involves an infinite hierarchy of beliefs. Such a hierarchy consists of an agent's beliefs about the state of the world, his beliefs about other agents' beliefs about the worlds, his beliefs about other agents' beliefs about other agents' beliefs about the worlds, etc. Economists and computer scientists differ, however, in the way they model beliefs. Economists prefer a probability-based framework, where belief is modeled as a probability distribution on the uncertainty space. In contrast, computer scientists prefer an information-based framework, where belief is modeled as a subset of the underlying space. The idea is that whatever is in the subset is believed to be possible, and whatever is not in the subset is believed to be impossible. We consider the question of when such an infinite hierarchy completely describes the uncertainty of the agents. We provide various necessary and sufficient conditions for this property. It turns out that the probability-based approach can be viewed as satisfying one of these conditions, which explains why the infinite hierarchy always completely describes the uncertainty of the agents in the probability-based approach. An interesting consequence of our conditions is that adequacy of an infinite hierarchy may depend on the "richness" of the states in the underlying state space. We also consider the question of whether an infinite hierarchy completely describes the uncertainty of the agents with respect to "interesting" sets of events and show that the answers depends on the definition of "interesting".

TARK Conference 1990 Conference Paper

A Nonstandard Approach to the Logical Omniscience Problem

• Ronald Fagin
• Joseph Y. Halpern
• Moshe Y. Vardi

We introduce a new approach to dealing with the well-known logical omniscience problem in epistemic logic. Instead of taking possible worlds where each world is a model of classical propositional logic, we take possible worlds which are models of a nonstandard propositional logic we call NPL, which is somewhat related to relevance logic. This approach gives new insights into the logic of implicit and explicit'belief considered by Levesque and Lakemeyer. In particular, we show that in a precise sense agents in the structures considered by Levesque and Lakemeyer are perfect reasoners in NPL.

STOC Conference 1989 Conference Paper

On omega-Automata and Temporal Logic (Preliminary Report)

• Muli Safra
• Moshe Y. Vardi

STOC Conference 1988 Conference Paper

Decidable Optimization Problems for Database Logic Programs (Preliminary Report)

• Stavros S. Cosmadakis
• Haim Gaifman
• Paris C. Kanellakis
• Moshe Y. Vardi

STOC Conference 1988 Conference Paper

Reasoning about Knowledge and Time in Asynchronous Systems

• Joseph Y. Halpern
• Moshe Y. Vardi

TCS Journal 1987 Journal Article

The complementation problem for Büchi automata with applications to temporal logic

• A. Prasad Sistla
• Moshe Y. Vardi
• Pierre Wolper

STOC Conference 1987 Conference Paper

The Decision Problem for the Probabilities of Higher-Order Properties

• Phokion G. Kolaitis
• Moshe Y. Vardi

TARK Conference 1986 Conference Paper

Knowledge and Implicit Knowledge in a Distributed Environment: Preliminary Report

• Ronald Fagin
• Moshe Y. Vardi

TARK Conference 1986 Conference Paper

On Epistemic Logic and Logical Omniscience

• Moshe Y. Vardi

We consider the logical omniscience problem of epistemic logic. We argue that the problem is due to the way in which knowledge and beliefare captured in Hintikka's possible worlds semantics. We describe an alternative approach in which propositions are sets of worlds, and knowledge and belief are simply a listof propositions for each agent. The problem of the circularityin the definitionis solved by giving a constructive definitionof beliefand knowledge worlds. We show how to incorporate notions such as reasoning and context of use in our model. We also demonstrate the power of our approach by showing how we can emulate in it other epistemic models.

STOC Conference 1986 Conference Paper

Reasoning about Fair Concurrent Programs

• Costas Courcoubetis
• Moshe Y. Vardi
• Pierre Wolper

STOC Conference 1986 Conference Paper

The Complexity of Reasoning about Knowledge and Time: Extended Abstract

• Joseph Y. Halpern
• Moshe Y. Vardi

IJCAI Conference 1985 Conference Paper

A Model-Theoretic Analysis of Monotonic Knowledge

• Moshe Y. Vardi

STOC Conference 1985 Conference Paper

An Internal Semantics for Modal Logic: Preliminary Report

• Ronald Fagin
• Moshe Y. Vardi

FOCS Conference 1985 Conference Paper

Automatic Verification of Probabilistic Concurrent Finite-State Programs

• Moshe Y. Vardi

The verification problem for probabilistic concurrent finite-state program is to decide whether such a program satisfies its linear temporal logic specification. We describe an automata-theoretic approach, whereby probabilistic quantification over sets of computations is reduced to standard quantification over individual computations. Using new determinization construction for ω-automata, we manage to improve the time complexity of the algorithm by two exponentials. The time complexity of the final algorithm is polynomial in the size of the program and doubly exponential in the size of the specification.

TCS Journal 1985 Journal Article

Formal systems for join dependencies

• Catriel Beeri
• Moshe Y. Vardi

STOC Conference 1985 Conference Paper

Improved Upper and Lower Bounds for Modal Logics of Programs: Preliminary Report

• Moshe Y. Vardi
• Larry J. Stockmeyer

FOCS Conference 1984 Conference Paper

A Model-Theoretic Analysis of Knowledge: Preliminary Report

• Ronald Fagin
• Joseph Y. Halpern
• Moshe Y. Vardi

Understanding knowledge is a fundamental issue in many disciplines. In computer science, knowledge arises not only in the obvious contexts (such as knowledge-based systems), but also in distributed systems (where the goal is to have each processor "know" something, as in Byzantine agreement). A general semantic model of knowledge is introduced, to allow reasoning about statements such as "He knows that I know whether or not she knows whether or not it is raining. " This approach more naturally models a state of knowledge than previous proposals (including Kripke structures). Using this notion of model, a model theory for knowledge is developed. This theory enables one to interpret such notions as a "finite amount of information" and "common knowledge" in different contexts.

STOC Conference 1984 Conference Paper

Automata Theoretic Techniques for Modal Logics of Programs (Extended Abstract)

• Moshe Y. Vardi
• Pierre Wolper

FOCS Conference 1983 Conference Paper

Reasoning about Infinite Computation Paths (Extended Abstract)

• Pierre Wolper
• Moshe Y. Vardi
• A. Prasad Sistla

We investigate extensions of temporal logic by finite automata on infinite words. There are three different types of acceptance conditions (finite, looping and repeating) that one can give for these finite automata. This gives rise to three different logics. It turns out, however. that these logics have the same expressive power but differ in the complexity of their decision problem. We also investigate the addition of alternation and show that it does not increase the complexity of the decision problem.

STOC Conference 1983 Conference Paper

Unary Inclusion Dependencies have Polynomial Time Inference Problems (Extended Abstract)

• Paris C. Kanellakis
• Stavros S. Cosmadakis
• Moshe Y. Vardi

FOCS Conference 1982 Conference Paper

On Decomposition of Relational Databases

• Moshe Y. Vardi

A central issue in relational database theory is that of decomposition. It has been agreed that decompositions should be injective, so as not to lose information, and surjective, so they decompose a relation into independent components. Injectiveness and surjectiveness are in general second-order notions. We show here how to express these notions in a first-order manner, assuming that we are dealing only with first-order constraints. As a consequence we get that the reconstruction map, which is the inverse to the decomposition map, is also first-order, but is not necessarily the natural join. This result is derived by applying Beth's Definability Theorem from model theory. For the case that the constraints used are implicational dependencies, we derive the exact syntactic form of the reconstruction map, and show that if the decomposition map is both injective and surjective then the reconstruction map is the natural join.

STOC Conference 1982 Conference Paper

The Complexity of Relational Query Languages (Extended Abstract)

• Moshe Y. Vardi

FOCS Conference 1981 Conference Paper

Global Decision Problems for Relational Databases

• Moshe Y. Vardi

Database dependencies are first-order sentences describing the semantics of databases. Decision problems concerning dependencies divide into local problem, such as whether a set of dependencies logically implies another dependency, and global problems, such as whether a set of dependencies is redundant. In this paper we investigate global problems, that of recognizing properties of sets of dependencies. The main result is a negative result in the spirit of Adjan-Markov-Rabin result for global properties of finitely presented semigroups and groups. We show that the decision problem for any property which is wellbehaved in a certain sense (specifically, if it is nice, non-trivial and hereditary) is recursively unsolvable.