Extended Temporal Logic Revisited. - Orna Kupferman; Nir Piterman; Moshe Y. Vardi (CONCUR, 2001)

Model Checking Linear Properties of Prefix-Recognizable Systems. - Orna Kupferman; Nir Piterman; Moshe Y. Vardi (CAV, 2002)

Pushdown Specifications. - Orna Kupferman; Nir Piterman; Moshe Y. Vardi (LPAR, 2002)

Fair Equivalence Relations. - Orna Kupferman; Nir Piterman; Moshe Y. Vardi (Verification: Theory and Practice, 2003)

Enhanced Vacuity Detection in Linear Temporal Logic. - Roy Armoni; Limor Fix; Alon Flaisher; Orna Grumberg; Nir Piterman; Andreas Tiemeyer; Moshe Y. Vardi (CAV, 2003)

Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems. - Nir Piterman; Moshe Y. Vardi (LICS, 2003)

From bidirectionality to alternation. - Nir Piterman; Moshe Y. Vardi (Theor. Comput. Sci., 2003)

Global Model-Checking of Infinite-State Systems. - Nir Piterman; Moshe Y. Vardi (CAV, 2004)

Combining State-Based and Scenario-Based Approaches in Modeling Biological Systems. - Jasmin Fisher; David Harel; E. Jane Albert Hubbard; Nir Piterman; Michael J. Stern; Naamah Swerdlin (CMSB, 2004)

Liveness with Incomprehensible Ranking. - Yi Fang 001; Nir Piterman; Amir Pnueli; Lenore D. Zuck (TACAS, 2004)

SAT-based Induction for Temporal Safety Properties. - Roy Armoni; Limor Fix; Ranan Fraer; Scott Huddleston; Nir Piterman; Moshe Y. Vardi (BMC@CAV, 2004)

Bridging the gap between fair simulation and trace inclusion. - Yonit Kesten; Nir Piterman; Amir Pnueli (Inf. Comput., 2005)

Inferring Network Invariants Automatically. - Olga Grinchtein; Martin Leucker; Nir Piterman (IJCAR, 2006)

Minimizing Generalized Büchi Automata. - Sudeep Juvekar; Nir Piterman (CAV, 2006)

Safraless Compositional Synthesis. - Orna Kupferman; Nir Piterman; Moshe Y. Vardi (CAV, 2006)

Solving Games Without Determinization. - Thomas A. Henzinger; Nir Piterman (CSL, 2006)

Faster Solutions of Rabin and Streett Games. - Nir Piterman; Amir Pnueli (LICS, 2006)

Synthesis of Reactive(1) Designs. - Nir Piterman; Amir Pnueli; Yaniv Sa'ar (VMCAI, 2006)

Liveness with invisible ranking. - Yi Fang 001; Nir Piterman; Amir Pnueli; Lenore D. Zuck (Int. J. Softw. Tools Technol. Transf., 2006)

Interactive presentation: Automatic hardware synthesis from specifications: a case study. - Roderick Bloem; Stefan J. Galler; Barbara Jobstmann; Nir Piterman; Amir Pnueli; Martin Weiglhofer (DATE, 2007)

Generalized Parity Games. - Krishnendu Chatterjee; Thomas A. Henzinger; Nir Piterman (FoSSaCS, 2007)

Specify, Compile, Run: Hardware from PSL. - Roderick Bloem; Stefan J. Galler; Barbara Jobstmann; Nir Piterman; Amir Pnueli; Martin Weiglhofer (COCV@ETAPS, 2007)

From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata. - Nir Piterman (Log. Methods Comput. Sci., 2007)

Predictive Modeling of Signaling Crosstalk during C. elegans Vulval Development. - Jasmin Fisher; Nir Piterman; Alex Hajnal; Thomas A. Henzinger (PLoS Comput. Biol., 2007)

Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions. - Jasmin Fisher; Thomas A. Henzinger; Maria Mateescu; Nir Piterman (FMSB, 2008)

Hintikka Games for PCTL on Labeled Markov Chains. - Harald Fecher; Michael Huth 001; Nir Piterman; Daniel Wagner 002 (QEST, 2008)

Algorithms for Büchi Games - Krishnendu Chatterjee; Thomas A. Henzinger; Nir Piterman (CoRR, 2008)

Three-Valued Abstractions of Markov Chains: Completeness for a Sizeable Fragment of PCTL. - Michael Huth 001; Nir Piterman; Daniel Wagner 002 (FCT, 2009)

Lower Bounds on Witnesses for Nonemptiness of Universal Co-Büchi Automata. - Orna Kupferman; Nir Piterman (FoSSaCS, 2009)

Computational modeling of the EGFR network elucidates control mechanisms regulating signal dynamics. - Dennis Y. Q. Wang; Luca Cardelli; Andrew Phillips; Nir Piterman; Jasmin Fisher (BMC Syst. Biol., 2009)

A workbench for preprocessor design and evaluation: toward benchmarks for parity games. - Michael Huth 001; Nir Piterman; Huaxin Wang (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2009)

From liveness to promptness. - Orna Kupferman; Nir Piterman; Moshe Y. Vardi (Formal Methods Syst. Des., 2009)

An Automata-Theoretic Approach to Infinite-State Systems. - Orna Kupferman; Nir Piterman; Moshe Y. Vardi (Essays in Memory of Amir Pnueli, 2010)

From Mtl to Deterministic Timed Automata. - Dejan Nickovic; Nir Piterman (FORMATS, 2010)

Synthesis of live behaviour models. - Nicolás D'Ippolito; Víctor A. Braberman; Nir Piterman; Sebastián Uchitel (SIGSOFT FSE, 2010)

Strategy logic. - Krishnendu Chatterjee; Thomas A. Henzinger; Nir Piterman (Inf. Comput., 2010)

PCTL model checking of Markov chains: Truth and falsity as winning strategies in games. - Harald Fecher; Michael Huth 001; Nir Piterman; Daniel Wagner 002 (Perform. Evaluation, 2010)

Dynamic Reactive Modules. - Jasmin Fisher; Thomas A. Henzinger; Dejan Nickovic; Nir Piterman; Anmol V. Singh; Moshe Y. Vardi (CONCUR, 2011)

The Only Way Is Up. - Jasmin Fisher; Nir Piterman; Moshe Y. Vardi (FM, 2011)

Concurrent Small Progress Measures. - Michael Huth 001; Jim Huan-Pu Kuo; Nir Piterman (Haifa Verification Conference, 2011)

The Rabin Index of Parity Games - (Extended Abstract). - Michael Huth 001; Jim Huan-Pu Kuo; Nir Piterman (Haifa Verification Conference, 2011)

Synthesis of live behaviour models for fallible domains. - Nicolás D'Ippolito; Víctor A. Braberman; Nir Piterman; Sebastián Uchitel (ICSE, 2011)

p-Automata and Obligation Games. - Nir Piterman (TIME, 2011)

Proving Stabilization of Biological Systems. - Byron Cook; Jasmin Fisher; Elzbieta Krepska; Nir Piterman (VMCAI, 2011)

LTL generalized model checking revisited. - Patrice Godefroid; Nir Piterman (Int. J. Softw. Tools Technol. Transf., 2011)

Bma: Visual Tool for Modeling and Analyzing Biological Networks. - David Benqué; Sam Bourton; Caitlin Cockerton; Byron Cook; Jasmin Fisher; Samin Ishtiaq; Nir Piterman; Alex S. Taylor; Moshe Y. Vardi (CAV, 2012)

The Modal Transition System Control Problem. - Nicolás D'Ippolito; Víctor A. Braberman; Nir Piterman; Sebastián Uchitel (FM, 2012)

Predictive Modelling of Stem Cell Differentiation and Apoptosis in C. elegans. - Antje Beyer; Ralf Eberhard; Nir Piterman; Michael O. Hengartner; Alex Hajnal; Jasmin Fisher (IPCAT, 2012)

Effective Synthesis of Asynchronous Systems from GR(1) Specifications. - Uri Klein; Nir Piterman; Amir Pnueli (VMCAI, 2012)

Synthesis of Reactive(1) designs. - Roderick Bloem; Barbara Jobstmann; Nir Piterman; Amir Pnueli; Yaniv Sa'ar (J. Comput. Syst. Sci., 2012)

p-Automata: New foundations for discrete-time probabilistic verification. - Michael Huth 001; Nir Piterman; Daniel Wagner 002 (Perform. Evaluation, 2012)

Model-Checking Signal Transduction Networks through Decreasing Reachability Sets. - Koen Claessen; Jasmin Fisher; Samin Ishtiaq; Nir Piterman; Qinsi Wang (CAV, 2013)

At the interface of biology and computation. - Alex S. Taylor; Nir Piterman; Samin Ishtiaq; Jasmin Fisher; Byron Cook; Caitlin Cockerton; Sam Bourton; David Benqué (CHI, 2013)

Fatal Attractors in Parity Games. - Michael Huth 001; Jim Huan-Pu Kuo; Nir Piterman (FoSSaCS, 2013)

Provably correct continuous control for high-level robot behaviors with actions of arbitrary execution durations. - Vasumathi Raman; Nir Piterman; Hadas Kress-Gazit (ICRA, 2013)

Controller synthesis: from modelling to enactment. - Víctor A. Braberman; Nicolás D'Ippolito; Nir Piterman; Daniel Sykes; Sebastián Uchitel (ICSE, 2013)

Synthesis from Temporal Specifications: New Applications in Robotics and Model-Driven Development. - Nir Piterman (MFCS, 2013)

Synthesis of biological models from mutation experiments. - Ali Sinan Köksal; Yewen Pu; Saurabh Srivastava 001; Rastislav Bodík; Jasmin Fisher; Nir Piterman (POPL, 2013)

The Rabin index of parity games. - Michael Huth 001; Jim Huan-Pu Kuo; Nir Piterman (GandALF, 2013)

Synthesizing nonanomalous event-based controllers for liveness goals. - Nicolás D'Ippolito; Víctor A. Braberman; Nir Piterman; Sebastián Uchitel (ACM Trans. Softw. Eng. Methodol., 2013)

Controllability in Partial and Uncertain Environments. - Nicolás D'Ippolito; Víctor A. Braberman; Nir Piterman; Sebastián Uchitel (ACSD, 2014)

Finding Instability in Biological Models. - Byron Cook; Jasmin Fisher; Benjamin A. Hall; Samin Ishtiaq; Garvit Juniwal; Nir Piterman (CAV, 2014)

Faster temporal reasoning for infinite-state programs. - Byron Cook; Heidy Khlaaf; Nir Piterman (FMCAD, 2014)

Backward Analysis via over-Approximate Abstraction and under-Approximate Subtraction. - Alexey Bakhirkin; Josh Berdine; Nir Piterman (SAS, 2014)

Fatal Attractors in Parity Games: Building Blocks for Partial Solvers. - Michael Huth 001; Jim Huan-Pu Kuo; Nir Piterman (CoRR, 2014)

On Automation of CTL* Verification for Infinite-State Systems. - Byron Cook; Heidy Khlaaf; Nir Piterman (CAV (1), 2015)

Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data. - Jasmin Fisher; Ali Sinan Köksal; Nir Piterman; Steven Woodhouse (CAV (1), 2015)

A Modelling Framework for Cyber-Physical System Resilience. - Manuela-Luminita Bujorianu; Nir Piterman (CyPhy, 2015)

A Recursive Probabilistic Temporal Logic. - Pablo F. Castro; Cecilia Kilmurray; Nir Piterman (ICFEM, 2015)

A Forward Analysis for Recurrent Sets. - Alexey Bakhirkin; Josh Berdine; Nir Piterman (SAS, 2015)

Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics. - Pablo F. Castro; Cecilia Kilmurray; Nir Piterman (STACS, 2015)

Fairness for Infinite-State Systems. - Byron Cook; Heidy Khlaaf; Nir Piterman (TACAS, 2015)

The Rabin index of parity games: Its complexity and approximation. - Michael Huth 001; Jim Huan-Pu Kuo; Nir Piterman (Inf. Comput., 2015)

Timing Semantics for Abstraction and Execution of Synthesized High-Level Robot Control. - Vasumathi Raman; Nir Piterman; Cameron Finucane; Hadas Kress-Gazit (IEEE Trans. Robotics, 2015)

Static Analysis of Parity Games: Alternating Reachability Under Parity. - Michael Huth 001; Jim Huan-Pu Kuo; Nir Piterman (Semantics, Logics, and Calculi, 2016)

Safety Verification of Piecewise-Deterministic Markov Processes. - Rafael Wisniewski; Christoffer Sloth; Manuela-Luminita Bujorianu; Nir Piterman (HSCC, 2016)

Finding Recurrent Sets with Backward Analysis and Trace Partitioning. - Alexey Bakhirkin; Nir Piterman (TACAS, 2016)

T2: Temporal Property Verification. - Marc Brockschmidt; Byron Cook; Samin Ishtiaq; Heidy Khlaaf; Nir Piterman (TACAS, 2016)

BTR: training asynchronous Boolean models using single-cell expression data. - Chee Yee Lim; Huange Wang; Steven Woodhouse; Nir Piterman; Lorenz Wernisch; Jasmin Fisher; Berthold Göttgens (BMC Bioinform., 2016)

Bringing LTL Model Checking to Biologists. - Zara Ahmed; David Benqué; Sergey Berezin; Anna Caroline E. Dahl; Jasmin Fisher; Benjamin A. Hall; Samin Ishtiaq; Jay Nanavati; Nir Piterman; Maik Riechert; Nikita Skoblov (VMCAI, 2017)

Equivalence of Probabilistic mu -Calculus and p-Automata. - Claudia Cauli; Nir Piterman (CIAA, 2017)

Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems. - Byron Cook; Heidy Khlaaf; Nir Piterman (J. ACM, 2017)

Obligation Blackwell Games and P-Automata. - Krishnendu Chatterjee; Nir Piterman (J. Symb. Log., 2017)

Advances in verification presented in TACAS'13. - Nir Piterman (Int. J. Softw. Tools Technol. Transf., 2017)

Interaction Models and Automated Control under Partial Observable Environments. - Daniel Alfredo Ciolek; Víctor A. Braberman; Nicolás D'Ippolito; Nir Piterman; Sebastián Uchitel (IEEE Trans. Software Eng., 2017)

SCNS: a graphical tool for reconstructing executable regulatory networks from single-cell genomic data. - Steven Woodhouse; Nir Piterman; Christoph M. Wintersteiger; Berthold Göttgens; Jasmin Fisher (BMC Syst. Biol., 2018)

Coverability: Realizability Lower Bounds. - Krishnendu Chatterjee; Nir Piterman (CoRR, 2018)

Temporal Logic and Fair Discrete Systems. - Nir Piterman; Amir Pnueli (Handbook of Model Checking, 2018)

Combinations of Qualitative Winning for Stochastic Parity Games. - Krishnendu Chatterjee; Nir Piterman (CONCUR, 2019)

Environmentally-Friendly GR(1) Synthesis. - Rupak Majumdar; Nir Piterman; Anne-Kathrin Schmuck (TACAS (2), 2019)

A Computational Framework for Adaptive Systems and its Verification. - Yehia Abd Alrahman; Giuseppe Perelli; Nir Piterman (CoRR, 2019)

Using State Space Exploration to Determine How Gene Regulatory Networks Constrain Mutation Order in Cancer Evolution. - Matthew A. Clarke; Steven Woodhouse; Nir Piterman; Benjamin A. Hall; Jasmin Fisher (Automated Reasoning for Systems Biology and Medicine, 2019)

Reconfigurable Interaction for MAS Modelling. - Yehia Abd Alrahman; Giuseppe Perelli; Nir Piterman (AAMAS, 2020)

The 3rd Controlled Adaptation of Self-adaptive Systems (CASaS) (NII Shonan Meeting 153). - Kenji Tei; Nir Piterman; Javier Cámara 001 (NII Shonan Meet. Rep., 2020)

Synthesis of Run-To-Completion Controllers for Discrete Event Systems. - Yehia Abd Alrahman; Víctor A. Braberman; Nicolás D'Ippolito; Nir Piterman; Sebastián Uchitel (ACC, 2021)

Incorporating Monitors in Reactive Synthesis Without Paying the Price. - Shaun Azzopardi; Nir Piterman; Gerardo Schneider (ATVA, 2021)

Pre-deployment Security Assessment for Cloud Services Through Semantic Reasoning. - Claudia Cauli; Meng Li; Nir Piterman; Oksana Tkachuk (CAV (1), 2021)

Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning (Extended Abstract). - Claudia Cauli; Meng Li; Nir Piterman; Oksana Tkachuk (Description Logics, 2021)

Closed- and Open-world Reasoning in DL-Lite for Cloud Infrastructure Security (Extended Abstract). - Claudia Cauli; Magdalena Ortiz 001; Nir Piterman (Description Logics, 2021)

Closed- and Open-world Reasoning in DL-Lite for Cloud Infrastructure Security. - Claudia Cauli; Magdalena Ortiz 001; Nir Piterman (KR, 2021)

Modelling and verification of reconfigurable multi-agent systems. - Yehia Abd Alrahman; Nir Piterman (Auton. Agents Multi Agent Syst., 2021)

Interleaving & Reconfigurable Interaction: Separating Choice from Scheduling using Glue. - Yehia Abd Alrahman; Mauricio Martel; Nir Piterman (CoRR, 2021)

R-CHECK: A Model Checker for Verifying Reconfigurable MAS. - Yehia Abd Alrahman; Shaun Azzopardi; Nir Piterman (AAMAS, 2022)

A Survey on Satisfiability Checking for the μ-Calculus Through Tree Automata. - Daniel Hausmann 001; Nir Piterman (Principles of Systems Design, 2022)

Actions over Core-Closed Knowledge Bases. - Claudia Cauli; Magdalena Ortiz 001; Nir Piterman (IJCAR, 2022)

A PO Characterisation of Reconfiguration. - Yehia Abd Alrahman; Mauricio Martel; Nir Piterman (ICTAC, 2022)

Model Checking Reconfigurable Interacting Systems. - Yehia Abd Alrahman; Shaun Azzopardi; Nir Piterman (ISoLA (3), 2022)

Runtime Verification Meets Controller Synthesis. - Shaun Azzopardi; Nir Piterman; Gerardo Schneider (ISoLA (1), 2022)

Control and Discovery of Environment Behaviour. - Maureen Keegan; Víctor A. Braberman; Nicolás D'Ippolito; Nir Piterman; Sebastián Uchitel (IEEE Trans. Software Eng., 2022)

ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae. - Shaun Azzopardi; David Lidell; Nir Piterman; Gerardo Schneider (ATVA, 2023)

Correct-by-Design Teamwork Plans for Multi-Agent Systems. - Yehia Abd Alrahman; Nir Piterman (CoRR, 2023)

Symbolic Reactive Synthesis for the Safety and EL-fragment of LTL. - Daniel Hausmann 001; Mathieu Lehaut; Nir Piterman (CoRR, 2023)

Correct-by-Construction Design of Contextual Robotic Missions Using Contracts. - Piergiuseppe Mallozzi; Nir Piterman; Pierluigi Nuzzo 002; Gerardo Schneider; Patrizio Pelliccione (CoRR, 2023)

LTL Synthesis on Infinite-State Arenas defined by Programs. - Shaun Azzopardi; Nir Piterman; Gerardo Schneider; Luca Di Stefano 001 (CoRR, 2023)

Games for Efficient Supervisor Synthesis. - Daniel Hausmann 001; Prabhat Kumar Jha; Nir Piterman (IEEE Control. Syst. Lett., 2023)

Language support for verifying reconfigurable interacting systems. - Yehia Abd Alrahman; Shaun Azzopardi; Luca Di Stefano 001; Nir Piterman (Int. J. Softw. Tools Technol. Transf., 2023)

Distribution of Reconfiguration Languages Maintaining Tree-Like Communication Topology. - Daniel Hausmann 001; Mathieu Lehaut; Nir Piterman (ATVA, 2024)

Faster and Smaller Solutions of Obliging Games. - Daniel Hausmann 001; Nir Piterman (CONCUR, 2024)

Symbolic Solution of Emerson-Lei Games for Reactive Synthesis. - Daniel Hausmann 001; Mathieu Lehaut; Nir Piterman (FoSSaCS (1), 2024)

Fair ω-Regular Games. - Daniel Hausmann 001; Nir Piterman; Irmak Saglam; Anne-Kathrin Schmuck (FoSSaCS (1), 2024)

Attributed Point-to-Point Communication in R-CHECK. - Yehia Abd Alrahman; Shaun Azzopardi; Luca Di Stefano 001; Nir Piterman (ISoLA (2), 2024)

A Direct Translation from LTL with Past to Deterministic Rabin Automata. - Shaun Azzopardi; David Lidell; Nir Piterman (MFCS, 2024)

Measuring the Gain of Reconfigurable Communication. - Mathieu Lehaut; Nir Piterman (GandALF, 2024)

Full LTL Synthesis over Infinite-State Arenas. - Shaun Azzopardi; Luca Di Stefano 001; Nir Piterman; Gerardo Schneider (CAV (4), 2025)

On Reconfigurable Bisimulation, with an Application to the Distributed Synthesis Problem. - Yehia Abd Alrahman; Nir Piterman (CoRR, 2025)

Engineering an LTLf Synthesis Tool. - Alexandre Duret-Lutz; Shufang Zhu 001; Nir Piterman; Giuseppe De Giacomo; Moshe Y. Vardi (CoRR, 2025)