Online Publications

Easy Complementation of History-Deterministic Buchi Automata
ATVA 24 paper with Bader Abu Radi and Ofer Leshkowitz
Abstract PDF Bibtex entry

Games with Weighted Multiple Objectives
ATVA 24 paper with Noam Shenwald
Abstract PDF Bibtex entry

Playing Games on Automata
ATVA 24 paper
Abstract PDF Bibtex entry

Restricted Flow Games
Javier 60 paper with Ravid Alon
Abstract PDF Bibtex entry

Synthesis with Privacy Against an Observer
FoSSaCS 24 paper with Ofer Leshkowitz and Naama Shamash Halevy
Abstract PDF Bibtex entry

Monotonicity Characterizations of Regular Languages
FST & TCS 23 paper with Yoav Feinstein
Abstract PDF Bibtex entry

Games with Trading of Control
CONCUR 23 paper with Noam Shenwald
Abstract PDF Bibtex entry

On Semantically-Deterministic Automata
ICALP 23 paper with Bader Abu Radi
Abstract PDF Bibtex entry

Using the Past for Resolving the Future
Frontiers 22 paper
Abstract PDF Bibtex entry

Synthesis of Privacy-Preserving Systems
FST & TCS 22 paper with Ofer Leshkowitz
Abstract PDF Bibtex entry

Minimization of Automata for Liveness Languages
ATVA 22 paper with Bader Abu Radi
Abstract PDF Bibtex entry

Energy Games with Resource-Bounded Environments
CONCUR 22 paper with Naama Shamash Halevy
Abstract PDF Bibtex entry

Lazy Regular Sensing
DCFS 22 paper with Asaf Petruschka
Abstract PDF Bibtex entry

The Complexity of LTL Rational Synthesis
TACAS 22 paper with Noam Shenwald
Abstract PDF Bibtex entry

A Hierarchy of Nondeterminism
MFCS 21 paper with Bader Abu Radi and Ofer Leshkowitz
Abstract PDF Bibtex entry

Certifying DFA Bounds for Recognition and Separation
ATVA 21 paper with Nir Lavee and Salomon Sickert
Abstract PDF Bibtex entry

Perspective Multi-Player Games
LICS 21 paper with Noam Shenwald
Abstract PDF Bibtex entry

Certifying Inexpressibility
FoSSaCS 21 paper with Salomon Sickert
Abstract PDF Bibtex entry

Perspective Games with Notifications
FST & TCS 20 paper with Noam Shenwald
Abstract PDF Bibtex entry

Mutually Accepting Capacitated Automata
DCFS 20 paper with Ravid Alon
Abstract PDF Bibtex entry

Canonicity in GFG and Transition-Based Automata
GANDALF 20 paper with Bader Abu Radi
Abstract PDF Bibtex entry

Unary Prime Languages
MFCS 20 paper with Nicolas Mazzocchi and Ismael Jecker
Abstract PDF Bibtex entry

On Repetition Languages
MFCS 20 paper with Ofer Leshkowitz
Abstract PDF Bibtex entry

On (I/O)-aware Good-For-Games Automata
ATVA 20 paper with Rachel Faran
Abstract PDF Bibtex entry

Good-Enough Synthesis
CAV 20 paper with Shaull Almagor
Abstract PDF Bibtex entry

Coverage and Vacuity in Network Formation Games
CSL 20 paper with Gili Bielous
Abstract PDF Bibtex entry

On Synthesis of Specifications with Arithmetic
SOFSEM 20 paper with Rachel Faran
Abstract PDF Bibtex entry

Register-Bounded Synthesis
CONCUR 19 paper with Ayrat Khalimov
Abstract PDF Bibtex entry

Reasoning about Quality and Fuzziness of Strategic Behaviours
IJCAI 19 paper with Patricia Bouyer-Decitre, Nicolas Markey, Bastien Maubert, Nello Murano, and Giuseppe Perelli
Abstract PDF Bibtex entry

Minimizing GFG Transition-Based Automata
ICALP 19 paper with Bader Abu Radi
Abstract PDF Bibtex entry

Perspective Games
LICS 19 paper with Gal Vardi
Abstract PDF Bibtex entry

Alternating Reachability Games with Behavioral and Revenue Objectives
LPAR 18 paper with Tami Tamir
Abstract PDF Bibtex entry

LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
LPAR 18 paper with Rachel Faran
Abstract PDF Bibtex entry

Spanning-Tree Games
MFCS 18 paper with Dan Hefetz, Amir Lellouche, and Gal Vardi
Abstract PDF Bibtex entry

Timed Network Games with Clocks
MFCS 18 paper with Guy Avni and Shibashis Guha
Abstract PDF Bibtex entry

The Unfortunate-Flow Problem
ICALP 18 paper with Gal Vardi
Abstract PDF Bibtex entry

Synthesis of Controllable Nash Equilibria in Games with Quantitative Objectives
IJCAI 18 paper with Shaull Almagor and Giuseppe Perelli
Abstract PDF Bibtex entry

Timed Vacuity
FM 18 paper with Hana Chockler and Shibashis Guha
Abstract PDF Bibtex entry

Multi-Player Flow Games
AAMAS 18 paper with Shibashis Guha and Gal Vardi
Abstract PDF Bibtex entry

Flow Games
FST & TCS 17 paper with Gal Vardi and Moshe Y. Vardi
Abstract PDF Bibtex entry

How Deterministic are Good-For-Games Automata?
FST & TCS 17 paper with Udi Boker and Michal Skrzypczak
Abstract PDF Bibtex entry

Timed Network Games
MFCS 17 paper with Guy Avni and Shibashis Guha
Abstract PDF Bibtex entry

Flow Logic
CONCUR 17 paper with Gal Vardi
Abstract PDF Bibtex entry

An Abstraction-Refinement Methodology for Reasoning about Network Games
IJCAI 17 paper with Guy Avni and Shibashis Guha
Abstract PDF Bibtex entry

Quantitative Assume Guarantee Synthesis
CAV 17 paper with Shaull Almagor, Jan Oliver Ringert, and Yaron Velner
Abstract PDF Bibtex entry

Examining Classical Graph-Theory Problems From The Viewpoint of Formal-Verification Methods
STOC 17 paper
Abstract PDF Bibtex entry

A Parametrized Analysis of Algorithms on Hierarchical Graphs
DCFS 17 paper with Rachel Faran
Abstract PDF Bibtex entry

Hierarchical Network Formation Games
TACAS 17 paper with Tami Tamir
Abstract PDF Bibtex entry

Dynamic Resource Allocation Games
SAGT16 paper with Guy Avni and Thomas A. Henzinger
Abstract PDF Bibtex entry

Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis
CONCUR16 paper with Shaull Almagor and Yaron Velner
Abstract PDF Bibtex entry

Eulerian Paths with Regular Constraints
MFCS16 paper with Gal Vardi
Abstract PDF Bibtex entry

High-Quality Synthesis Against Stochastic Environments
CSL16 paper with Shaull Almagor
Abstract PDF Bibtex entry

On the Capacity of Capacitated Automata
LATA16 paper with Sarai Sheinvald
Abstract PDF Bibtex entry

The Sensing Cost of Monitoring and Synthesis
FST & TCS 15 paper with Shaull Almagor and Denis Kuperberg
Abstract PDF Bibtex entry

Congestion Games with Multisets of Resources and Applications in Synthesis
FST & TCS 15 paper with Guy Avni and Tami Tamir
Abstract PDF Bibtex entry

Spanning the Spectrum from Safety to Liveness
ATVA15 paper with Rachel Faran
Abstract PDF Bibtex entry

On Relative and Probabilistic Finite Counterability
CSL15 paper with Gal Vardi
Abstract PDF Bibtex entry

Repairing Multi-Player Games
CONCUR15 paper with Shaull Almagor and Guy Avni
Abstract PDF Bibtex entry

Inherent Vacuity in Lattice Automata
YURIFEST15 paper with Hila Gonen
Abstract PDF Bibtex entry

Stochastization of Weighted Automata
MFCS15 paper with Guy Avni
Abstract PDF Bibtex entry

Automata Theory and Model Checking
Chapter in the Handbook of Model Checking
Abstract PDF Bibtex entry

Synthesis with Rational Environments
EUMAS14 paper with Giuseppe Perelli and Moshe Y. Vardi
Abstract PDF Bibtex entry

Properties and Utilization of Capacitated Automata
FST & TCS 14 paper with Tami Tamir
Abstract PDF Bibtex entry

Regular Sensing
FST & TCS 14 paper with Shaull Almagor and Denis Kuperberg
Abstract PDF Bibtex entry

A Game-Theoretic Approach to Simulation of Data-Parameterized Systems
ATVA 14 paper with Orna Grumberg and Sarai Sheinvald
Abstract PDF Bibtex entry

Synthesis from Component Libraries with Cost
CONCUR 14 paper with Guy Avni
Abstract PDF Bibtex entry

Discounting in LTL
TACAS 14 paper with Shaull Almagor and Udi Boker
Abstract PDF Bibtex entry

Variations on Safety
TACAS 14 paper
Abstract PDF Bibtex entry

Network-Formation Games with Regular Objectives
FOSSACS 14 paper with Guy Avni and Tami Tamir
Abstract PDF Bibtex entry

Latticed-LTL Synthesis in the Presence of Noisy Inputs
FOSSACS 14 paper with Shaull Almagor
Abstract PDF Bibtex entry

When Does Abstraction Help?
IPL article with Guy Avni
Abstract PDF Bibtex entry

Attention-based Coverage Metrics
HVC 13 paper with Shoham Ben-David and Hana Chockler
Abstract PDF Bibtex entry

Prime Languages
MFCS 13 paper with Jonathan Mosheiff
Abstract PDF Bibtex entry

Profile Trees for Buchi Word Automata, with Application to Determinization
GANDALF 13 paper with Seth Fogarty, Moshe Y. Vardi, and Thomas Wilke
Abstract PDF Bibtex entry

Weighted Safety
ATVA 13 paper with Sigal Weiner, Matan Hasson, Eyal Pery, and Zohar Shevach
Abstract PDF Bibtex entry

A Framework for Ranking Vacuity Results
ATVA 13 paper with Shoham Ben-David
Abstract PDF Bibtex entry

An Automata-Theoretic Approach for Reasoning About Parameterized Systems and Specifications
ATVA 13 paper with Orna Grumberg and Sarai Sheinvald
Abstract PDF Bibtex entry

Formalizing and Reasoning about Quality
ICALP 13 paper with Shaull Almagor and Udi Boker
Abstract PDF Bibtex entry

Nondeterminism in the Presence of a Diverse or Unknown Future
ICALP 13 paper with Udi Boker, Denis Kuperberg, and Michal Skrzypczak
Abstract PDF Bibtex entry

Automatic Generation of Quality Specifications
CAV 13 paper with Shaull Almagor and Guy Avni
Abstract PDF Bibtex entry

Parameterized Weighted Containment
FOSSACS 13 paper with Guy Avni
Abstract PDF Bibtex entry

Environment-Friendly Safety
HVC 12 paper with Sigal Weiner
Abstract PDF Bibtex entry

Approximating Deterministic Lattice Automata
ATVA 12 paper with Shulamit Halamish
Abstract PDF Bibtex entry

Model Checking Systems and Specifications with Parameterized Atomic Propositions
ATVA 12 paper with Orna Grumberg and Sarai Sheinvald
Abstract PDF Bibtex entry

Making Weighted Containment Feasible: A Heuristic Based on Simulation and Abstraction
CONCUR 12 paper with Guy Avni
Abstract PDF Bibtex entry

Recent Challenges and Ideas in Temporal Synthesis
SOFTSEM 12 paper
Abstract PDF Bibtex entry

Synthesis with Clairvoyance
HVC 11 paper with Dorsa Sadigh and Sanjit A. Seshia
Abstract PDF Bibtex entry

Max and Sum Semantics for Alternating Weighted Automata
ATVA 11 paper with Shaull Almagor
Abstract PDF Bibtex entry

Formal Analysis of Online Algorithms
ATVA 11 paper with Benajmin Aminof and Robby Lampert
Abstract PDF Bibtex entry

What's Decidable About Weighted Automata?
ATVA 11 paper with Shaull Almagor and Udi Boker
Abstract PDF Bibtex entry

An Abstraction-Refinement Framework for Trigger Querying
SAS 11 paper with Guy Avni
Abstract PDF Bibtex entry

Unifying Buchi Complementation Constructions
CSL 11 paper with Seth Fogarty, Moshe Y. Vardi, and Thomas Wilke
Abstract PDF Bibtex entry

Rigorous Approximated Determinization of Weighted Automata
LICS 11 paper with Benjamin Aminof and Robby Lampert
Abstract PDF Bibtex entry

Temporal Specifications with Accumulative Values
LICS 11 paper with Udi Boker, Krishnendu Chatterjee, and Thomas A. Henzinger
Abstract PDF Bibtex entry

Minimizing Deterministic Lattice Automata
FOSSACS 11 paper with Shulamit Halamish
Abstract PDF Bibtex entry

Co-Buching Them All
FOSSACS 11 paper with Udi Boker
Abstract PDF Bibtex entry

Temporal Synthesis for Bounded Systems and Environments
STACS 11 paper with Yoad Lustig, Moshe Y. Vardi, and Mihalis Yannakakis
Abstract PDF Bibtex entry

Partyizing Rabin and Streett
FST & TCS 10 paper with Udi Boker and Avital Steinitz
Abstract PDF Bibtex entry

The Blow-Up in Translating LTL to Deterministic Automata
MOCHART 10 paper with Adin Rosenberg
Abstract PDF Bibtex entry

Promptness in \omega-Automata
ATVA 10 paper with Shaull Almagor and Yoram Hirshfeld
Abstract PDF Bibtex entry

Alternation Removal in Buchi Automata
ICALP 10 paper with Udi Boker and Adin Rosenberg
Abstract PDF Bibtex entry

Coping with Selfish On-going Behaviors
LPAR 10 paper with Tami Tamir
Abstract PDF Bibtex entry

Synthesis of Trigger Properties
LPAR 10 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Variable Automata over Infinite Alphabets
LATA 10 paper with Orna Grumberg and Sarai Sheinvald
Abstract PDF Bibtex entry

Rational Synthesis
TACAS 10 paper with Dana Fisman and Yoad Lustig
Abstract PDF Bibtex entry

Improved Model Checking of Hierarchical Systems
VMCAI 10 paper with Benjamin Aminof and Aniello Murano
Abstract PDF Bibtex entry

Reasoning about Finite-State Switched Systems
HVC 09 paper with Dana Fisman
Abstract PDF Bibtex entry

Co-ing Buchi Made Tight and Useful
LICS 09 paper with Udi Boker
Abstract PDF Bibtex entry

Lower Bounds on Witnesses for Nonemptiness of Universal co-Buchi Automata
FOSSACS 09 paper with Nir Piterman
Abstract PDF Bibtex entry

Reasoning about Online Algorithms with Weighted Automata
SODA 09 paper with Benjamin Aminof and Robby Lampert
Abstract PDF Bibtex entry

A Framework for Inherent Vacuity
HVC 08 paper with Dana Fisman, Sarai Sheinvald, and Moshe Y. Vardi
Abstract PDF Bibtex entry

On the Relative Succinctness of Nondeterministic Buchi and co-Buchi Word Automata
LPAR 08 paper with Benjamin Aminof and Omer Lev
Abstract PDF Bibtex entry

A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance
FMCAD 08 paper with Wenchao Li and Sanjit S. Seshia
Abstract PDF Bibtex entry

Vacuity in Testing
TAP 08 paper with Thomas Ball
Abstract PDF Bibtex entry

On Verifying Fault Tolerance of Distributed Protocols
TACAS 08 paper with Dana Fisman and Yoad Lustig
Abstract PDF Bibtex entry

What Triggers a Behavior?
FMCAD 07 paper with Yoad Lustig
Abstract PDF Bibtex entry

Latticed Simulation Relations and Games
ATVA 07 paper with Yoad Lustig
Abstract PDF Bibtex entry

Tightening the Exchange Rate Between Automata
CSL 07 paper
Abstract PDF Bibtex entry

Leaping Loops in the Presence of Abstraction
CAV 07 paper with Thomas Ball and Mooly Sagiv
Abstract PDF Bibtex entry

From Liveness to Promptness
CAV 07 paper with Nir Piterman and Moshe Y. Vardi
Abstract PDF Bibtex entry

Lattice Automata
VMCAI 07 paper with Yoad Lustig
Abstract PDF Bibtex entry

Better Under-approximation of Programs by Hiding Variables
VMCAI 07 paper with Thomas Ball
Abstract PDF Bibtex entry

On Locally Checkable Properties
LPAR 06 paper with Yoad Lustig and Moshe Vardi
Abstract PDF Bibtex entry

On the Construction of Fine Automata for Safety Properties
ATVA 06 paper with Robby Lampert
Abstract PDF Bibtex entry

On The Succinctness of Nondeterminizm
ATVA 06 paper with Benjamin Aminof
Abstract PDF Bibtex entry

Sanity Checks in Formal Verification
CONCUR 06 paper
Abstract PDF Bibtex entry

Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words
CONCUR 06 paper with Sarai Sheinvald-Faragy
Abstract PDF Bibtex entry

Safraless Compositional Synthesis
CAV 06 paper with Nir Piterman and Moshe Y. Vardi
Abstract PDF Bibtex entry

Avoiding Determinization
LICS 06 paper
Abstract PDF Bibtex entry

An Abstraction-Refinement Framework for Multi-Agent Systems
LICS 06 paper with Thomas Ball
Abstract PDF Bibtex entry

Memoryful Branching-Time Logics
LICS 06 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Safraless Decision Procedures
FOCS 05 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Abstraction for Falsification
CAV 05 paper with Thomas Ball and Greta Yorsh
Abstract PDF Bibtex entry

Regular Vacuity
CHARME 05 paper with Doron Bustan, Alon Flaisher, Orna Grumberg, and Moshe Y. Vardi
Abstract PDF Bibtex entry

Verifying Quantitative Properties Using Bound Functions
CHARME 05 paper with Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, and Rupak Majumdar
Abstract PDF Bibtex entry

Complementation Constructions for Nondeterministic Automata on Infinite Words
TACAS 05 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Reasoning about Systems with Transition Fairness
LPAR 04 paper with Benjamin Aminof and Thomas Ball
Abstract PDF Bibtex entry

Typeness for \omega-Regular Automata
ATVA 04 paper with Gila Morgenstern and Aniello Murano
Abstract PDF Bibtex entry

Buchi Complementation Made Tighter
ATVA 04 paper with Ehud Friedgut and Moshe Y. Vardi
Abstract PDF Bibtex entry

A Measured Collapse of The Modal \mu-Calculus Alternation Hierarchy
STACS 04 paper with Doron Bustan and Moshe Y. Vardi
Abstract PDF Bibtex entry

From Complementation to Certification
TACAS 04 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Coverage Metrics for Formal Verification
CHARME 03 paper with Hana Chockler and Moshe Y. Vardi
Abstract PDF Bibtex entry

On Complementing Nondeterministic Buchi Automata
CHARME 03 paper with Sankar Gurumurthy, Fabio Somenzi, and Moshe Y. Vardi
Abstract PDF Bibtex entry

Formal Analysis of Scientific-Computation Methods
ADHS 03 paper with Gadi Auerbach
Abstract PDF Bibtex entry

\Pi_2 \cap \Sigma_2 = AFMC
ICALP 03 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

On the Universal and Existential Fragments of the \mu-Calculus
TACAS 03 paper with Thomas A. Henzinger and Rupak Majumdar
Abstract PDF Bibtex entry

Resets vs. Aborts in Linear Temporal Logic
TACAS 03 paper with Roi Armoni, Doron Bustan, and Moshe Y. Vardi
Abstract PDF Bibtex entry

Pushdown Specifications
LPAR 02 paper with Nir Piterman and Moshe Y. Vardi
Abstract PDF Bibtex entry

\omega-regular Languages are Testable with a Constant Number of Queries
RANDOM 02 paper with Hana Chockler
Abstract PDF Bibtex entry

Trading Probability for Fairness
CSL 02 paper with Marcin Jurdzinski and Thomas Henzinger
Abstract PDF Bibtex entry

An Improved Algorithm for the Membership Problem for Extended Regular Expressions
MFCS 02 paper with Sharon Zuhovitzky
Abstract PDF Bibtex entry

Coverage of implementations by simulating specifications
TCS 02 paper with Hana Chockler
Abstract PDF Bibtex entry

The Complexity of the Graded \mu-Calculus
CADE 02 paper with Ulrike Sattler and Moshe Y. Vardi
Abstract PDF Bibtex entry

Model Checking Linear Properties of Prefix-Recognizable Systems
CAV 02 paper with Nir Piterman and Moshe Y. Vardi
Abstract PDF Bibtex entry

Synthesis of Uninitialized Systems
ICALP 02 paper with Thomas A. Henzinger, Sriram C. Krishnan, and Freddy Y.C. Mang
Abstract PDF Bibtex entry

On Clopen Specifications
LPAR 01 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Extended Temporal Logic Revisited
CONCUR 01 paper with Nir Piterman and Moshe Y. Vardi
Abstract PDF Bibtex entry

A Practical Approach to Coverage in Model Checking
CAV 01 paper with Hana Chockler, Robert P. Kurshan, and Moshe Y. Vardi
Abstract PDF Bibtex entry

Synthesizing Distributed Systems
LICS 01 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

On the Complexity of Parity Word Automata
FOSSACS 01 paper with Valerie King and Moshe Y. Vardi
Abstract PDF Bibtex entry

Coverage Metrics for Temporal Logic Model Checking
TACAS 01 paper with Hana Chockler and Moshe Y. Vardi
Abstract PDF Bibtex entry

Fair Equivalence Relations
FST & TCS 00 paper with Nir Piterman and Moshe Y. Vardi
Abstract PDF Bibtex entry

Branching-Depth Hierarchies
EXPRESS 00 paper with Shoham Shamir and Eli Shamir
Abstract PDF Bibtex entry

\mu-Calculus Synthesis
MFCS 00 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Open Systems in Reactive Environments: Control and Synthesis
CONCUR 00 paper with P. Madhusudan, P.S. Thiagarajan, and Moshe Y. Vardi
Abstract PDF Bibtex entry

On the Behavioral Inheritance of State-Based Objects.
TOOLS 00 paper with David Harel
Abstract PDF Bibtex entry

An Automata-Theoretic Approach to Reasoning about Infinite-State Systems.
CAV 00 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Vacuity Detection in Temporal Model Checking.
CHARME 99 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Robust Satisfaction.
CONCUR 99 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Model Checking of Safety Properties.
CAV 99 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

The Weakness of Self-Complementation.
STACS 99 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Concurrent Reachability Games.
FOCS 98 paper with Luca de Alfaro and Thomas A. Henzinger
Abstract PDF Bibtex entry

Alternating Refinement Relations.
CONCUR 98 paper with Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi
Abstract PDF Bibtex entry

From Pre-historic to Post-modern Symbolic Model Checking.
CAV 98 paper with Thomas A. Henzinger and Shaz Qadeer
Abstract PDF Bibtex entry

Freedom, Weakness, and Determinism: From Linear-time to Branching-time.
LICS 98 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Weak Alternating Automata and Tree Automata Emptiness.
STOC 98 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Relating Linear and Branching Model Checking.
PROCOMET 98 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Modular Model Checking.
Compositionality 97 paper with Moshe Y. Vardi
Abstract PDF Bibtex entry

Alternating-Time Temporal Logic.
FOCS 97 paper with Rajeev Alur and Thomas A. Henzinger
Abstract PDF Bibtex entry

Existence of Reduction Hierarchies.
CSL 97 paper with Robert P. Kurshan and Mihalis Yannakakis.
Abstract PDF Bibtex entry

Synthesis with Incomplete Informatio.
ICTL 97 paper with Moshe Y. Vardi.
Abstract PDF Bibtex entry

On the Complexity of Verifying Concurrent Transition Systems.
CONCUR 97 paper with David Harel and Moshe Y. Vardi.
Abstract PDF Bibtex entry

Fair Simulation.
CONCUR 97 paper with Thomas A. Henzinger and Sriram Rajamani.
Abstract PDF Bibtex entry

Weak Alternating Automata are not That Weak.
ISTCS 97 paper with Moshe Y. Vardi.
Abstract PDF Bibtex entry

Module Checking Revisited.
CAV 97 paper with Moshe Y. Vardi.
Abstract PDF Bibtex entry

From Quantity to Quality.
HART 97 paper with Thomas A. Henzinger.
Abstract PDF Bibtex entry

A Space-efficient On-the-fly Algorithm for Real-time Model Checking.
CONCUR 96 paper with Thomas A. Henzinger and Moshe Y. Vardi.
Abstract PDF Bibtex entry

Not Checking for Closure under Stuttering.
SPIN 96 paper with Gerard Holzmann.
Abstract PDF Bibtex entry

Verification of Fair Transition Systems.
CAV 96 paper with Moshe Y. Vardi.
Abstract PDF Bibtex entry

Module Checking.
CAV 96 paper with Moshe Y. Vardi.
Abstract PDF Bibtex entry

Relating Word and Tree Automata.
LICS 96 paper with Samuel Safra and Moshe Y. Vardi.
Abstract PDF Bibtex entry

Model Checking for Branching-Time Temporal Logics.
Ph.D. Thesis.
Abstract PDF Bibtex entry

On the Complexity of Branching Modular Model Checking.
CONCUR 95 paper with Moshe Y. Vardi.
Abstract PDF Bibtex entry

Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions.
CAV 95 paper.
Abstract PDF Bibtex entry

Once and For all.
LICS 95 paper with Amir Pnueli.
Abstract PDF Bibtex entry

Buy One, Get One Free!!!
ICTL 94 paper with Orna Grumberg.
Abstract PDF Bibtex entry

An Automata-Theoretic Approach to Branching-Time Model Checking.
CAV 94 paper with Moshe Y. Vardi and Pierre Wolper.
Abstract PDF Bibtex entry

Branching-Time Temporal Logic and Tree Automata.
CONCUR 93 paper with Orna Grumberg.
Abstract PDF Bibtex entry

Back to Home page