Browsing by Author "Vardi, Moshe Y."
Now showing items 119 of 19

Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls*
Chakraborty, Supratik; Meel, Kuldeep S.; Vardi, Moshe Y. (20161128)Probabilistic inference via model counting has emerged as a scalable technique with strong formal guarantees, thanks to recent advances in hashingbased approximate counting. Stateoftheart hashingbased counting algorithms ... 
Bisimulation Minimization in an AutomataTheoretic Verification Framework
Fisler, Kathi; Vardi, Moshe Y. (19981027)Bisimulation is a seemingly attractive statespace minimization technique because it can be computed automatically and yields the smallest model preserving all mu calculus formulas. It is considered impractical for symbolic ... 
Fixpoint Logics, Relational Machines, and Computational Complexity
Abiteboul, Serge; Vardi, Moshe Y.; Vianu, Victor (19961011)We establish a general connection between fixpoint logic and complexity. On one side, we have fixpoint logic, parameterized by the choices of 1storder operators (inflationary or noninflationary) and iteration constructs ... 
Iterative Temporal Motion Planning for Hybrid Systems in Partially Unknown Environments
Maly, Matthew R.; Lahijanian, Morteza; Kavraki, Lydia E.; KressGazit, Hadas; Vardi, Moshe Y. (2013)This paper considers the problem of motion planning for a hybrid robotic system with complex and nonlinear dynamics in a partially unknown environment given a temporal logic specification. We employ a multilayered synergistic ... 
Linear Temporal Logic and Linear Dynamic Logic on Finite Traces
De Giacomo, Giuseppe; Vardi, Moshe Y. (2013)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 ... 
Module Checking
Kupferman, Orna; Vardi, Moshe Y.; Wolper, Pierre (19980222)In computer system design, we distinguish between closed and open systems. A closed system is a system whose behavior is completely determined by the state of the system. An open system is a system that interacts with its ... 
On computing minimal independent support and its applications to sampling and counting
Ivrii, Alexander; Malik, Sharad; Meel, Kuldeep S.; Vardi, Moshe Y. (2015)Constrained sampling and counting are two fundamental problems arising in domains ranging from artificial intelligence and security, to hardware and software testing. Recent approaches to approximate solutions for these ... 
Once and For All
Kupferman, Orna; Pnueli, Amir; Vardi, Moshe Y. (2012)It has long been known that pasttime operators add no expressive power to linear temporal logics. In this paper, we consider the extension of branching temporal logics with pasttime operators. Two possible views regarding ... 
Publication Culture in Computing Research
Mehlhorn, Kurt; Vardi, Moshe Y.; Herbstritt, Marc (2012)The dissemination of research results is an integral part of research and hence a crucial component for any scientific discipline. In the area of computing research, there have been raised concerns recently about its ... 
Reasoning about Strategies: on the Satisfiability Problem
Mogavero, Fabio; Murano, Aniello; Perelli, Giuseppe; Vardi, Moshe Y. (2017)Strategy Logic (SL, for short) has been introduced by Mogavero, Murano, and Vardi as a useful formalism for reasoning explicitly about strategies, as firstorder objects, in multiagent concurrent games. This logic turns ... 
Regular Real Analysis
Chaudhuri, Swarat; Sankaranarayanan, Sriram; Vardi, Moshe Y. (2013)We initiate the study of regular real analysis, or the analysis of real functions that can be encoded by automata on infinite words. It is known that ωautomata can be used to represent {relations} between real ... 
Relating Linear and Branching Model Checking
Kupferman, Orna; Vardi, Moshe Y. (19980608)The difference in the complexity of branching and linear model checking has been viewed as an argument in favor of the branching paradigm. In particular, the computational advantage of CTL model checking over LTL model ... 
Relentful Strategic Reasoning in 1 AlternatingTime Temporal Logic
Mogavero, Fabio; Murano, Aniello; Vardi, Moshe Y. (2014)Temporal logics are a well investigated formalism for the specification, verification, and synthesis of reactive systems. Within this family, AlternatingTime Temporal Logic (ATL , for short) has been introduced as a ... 
Solving PartialInformation Stochastic Parity Games
Nain, Sumit; Vardi, Moshe Y. (2013)We study onesided partialinformation 2player concurrent stochastic games with parity objectives. In such a game, one of the players has only partial visibility of the state of the game, while the other player has complete ... 
Synthesis from Probabilistic Components
Nain, Sumit; Lustig, Yoad; Vardi, Moshe Y. (2014)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. ... 
Unifying Büchi Complementation Constructions
Fogarty, Seth J.; Kupferman, Orna; Wilke, Thomas; Vardi, Moshe Y. (2013)Complementation of B\"uchi 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 ... 
Verification of Fair Transition Systems
Kupferman, Orna; Vardi, Moshe Y. (19970827)In program verification we check that an implementation meets its specification. Both the specification and the implementation describe the possible behaviors of the program, though at different levels of abstraction. We ... 
Verification of Open Systems
Vardi, Moshe Y. (19980404)In computer system design, we distinguish between closed and open systems. A closed system is a system whose behavior is completely determined by the state of the system. An open system is a system that interacts with its ... 
Why Is Modal Logic So Robustly Decidable?
Vardi, Moshe Y. (19970412)In the last 20 years modal logic has been applied to numerous areas of computer science, including artificial intelligence, program verification, hardware verification, database theory, and distributed computing. There are ...