Nir Piterman

CoRR, 2024

A Direct Translation from LTL with Past to Deterministic Rabin Automata.

[BibT_eX]

[DOI]

David Lidell

Proceedings of the 49th International Symposium on Mathematical Foundations of Computer Science, 2024

Attributed Point-to-Point Communication in R-CHECK.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Rigorous Engineering of Collective Adaptive Systems, 2024

Fair ømega-Regular Games.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2024

Symbolic Solution of Emerson-Lei Games for Reactive Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2024

Faster and Smaller Solutions of Obliging Games.

[BibT_eX]

[DOI]

Proceedings of the 35th International Conference on Concurrency Theory, 2024

2023

Language support for verifying reconfigurable interacting systems.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., December, 2023

Games for Efficient Supervisor Synthesis.

[BibT_eX]

[DOI]

Prabhat Kumar Jha

IEEE Control. Syst. Lett., 2023

Fair $ω$-Regular Games.

[BibT_eX]

[DOI]

CoRR, 2023

LTL Synthesis on Infinite-State Arenas defined by Programs.

[BibT_eX]

[DOI]

CoRR, 2023

Correct-by-Construction Design of Contextual Robotic Missions Using Contracts.

[BibT_eX]

[DOI]

Piergiuseppe Mallozzi

CoRR, 2023

Symbolic Reactive Synthesis for the Safety and EL-fragment of LTL.

[BibT_eX]

[DOI]

CoRR, 2023

Measuring the Gain of Reconfigurable Communication.

[BibT_eX]

[DOI]

CoRR, 2023

Correct-by-Design Teamwork Plans for Multi-Agent Systems.

[BibT_eX]

[DOI]

CoRR, 2023

ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2023

2022

Control and Discovery of Environment Behaviour.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2022

Runtime Verification Meets Controller Synthesis.

[BibT_eX]

[DOI]

Gerardo Schneider

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 2022

Model Checking Reconfigurable Interacting Systems.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning, 2022

A PO Characterisation of Reconfiguration.

[BibT_eX]

[DOI]

Mauricio Martel

Proceedings of the Theoretical Aspects of Computing - ICTAC 2022, 2022

Actions over Core-Closed Knowledge Bases.

[BibT_eX]

[DOI]

Magdalena Ortiz

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

A Survey on Satisfiability Checking for the μ-Calculus Through Tree Automata.

[BibT_eX]

[DOI]

Proceedings of the Principles of Systems Design, 2022

R-CHECK: A Model Checker for Verifying Reconfigurable MAS.

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems, 2022

2021

Interleaving & Reconfigurable Interaction: Separating Choice from Scheduling using Glue.

[BibT_eX]

[DOI]

Mauricio Martel

CoRR, 2021

Modelling and verification of reconfigurable multi-agent systems.

[BibT_eX]

[DOI]

Auton. Agents Multi Agent Syst., 2021

Closed- and Open-world Reasoning in DL-Lite for Cloud Infrastructure Security.

[BibT_eX]

[DOI]

Magdalena Ortiz

Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, 2021

Closed- and Open-world Reasoning in DL-Lite for Cloud Infrastructure Security (Extended Abstract).

[BibT_eX]

[DOI]

Magdalena Ortiz

Proceedings of the 34th International Workshop on Description Logics (DL 2021) part of Bratislava Knowledge September (BAKS 2021), 2021

Pre-Deployment Security Assessment for Cloud Services through Semantic Reasoning (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the 34th International Workshop on Description Logics (DL 2021) part of Bratislava Knowledge September (BAKS 2021), 2021

Pre-deployment Security Assessment for Cloud Services Through Semantic Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Incorporating Monitors in Reactive Synthesis Without Paying the Price.

[BibT_eX]

[DOI]

Gerardo Schneider

Proceedings of the Automated Technology for Verification and Analysis, 2021

Synthesis of Run-To-Completion Controllers for Discrete Event Systems.

[BibT_eX]

[DOI]

Proceedings of the 2021 American Control Conference, 2021

2020

The 3rd Controlled Adaptation of Self-adaptive Systems (CASaS) (NII Shonan Meeting 153).

[BibT_eX]

[DOI]

Kenji Tei

Javier Cámara

NII Shonan Meet. Rep., 2020

Reconfigurable Interaction for MAS Modelling.

[BibT_eX]

[DOI]

Giuseppe Perelli

Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems, 2020

2019

Using State Space Exploration to Determine How Gene Regulatory Networks Constrain Mutation Order in Cancer Evolution.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning for Systems Biology and Medicine, 2019

A Computational Framework for Adaptive Systems and its Verification.

[BibT_eX]

[DOI]

Giuseppe Perelli

CoRR, 2019

Environmentally-Friendly GR(1) Synthesis.

[BibT_eX]

[DOI]

Rupak Majumdar

Anne-Kathrin Schmuck

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Combinations of Qualitative Winning for Stochastic Parity Games.

[BibT_eX]

[DOI]

Proceedings of the 30th International Conference on Concurrency Theory, 2019

2018

Temporal Logic and Fair Discrete Systems.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Model Checking., 2018

Coverability: Realizability Lower Bounds.

[BibT_eX]

[DOI]

CoRR, 2018

SCNS: a graphical tool for reconstructing executable regulatory networks from single-cell genomic data.

[BibT_eX]

[DOI]

Steven Woodhouse

Christoph M. Wintersteiger

Berthold Göttgens

BMC Syst. Biol., 2018

2017

Interaction Models and Automated Control under Partial Observable Environments.

[BibT_eX]

[DOI]

Daniel Alfredo Ciolek

IEEE Trans. Software Eng., 2017

Advances in verification presented in TACAS'13.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2017

Obligation Blackwell Games and P-Automata.

[BibT_eX]

[DOI]

J. Symb. Log., 2017

Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems.

[BibT_eX]

[DOI]

J. ACM, 2017

Equivalence of Probabilistic \mu -Calculus and p-Automata.

[BibT_eX]

[DOI]

Proceedings of the Implementation and Application of Automata, 2017

Bringing LTL Model Checking to Biologists.

[BibT_eX]

[DOI]

Zara Ahmed

David Benqué

Sergey Berezin

Anna Caroline E. Dahl

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

2016

BTR: training asynchronous Boolean models using single-cell expression data.

[BibT_eX]

[DOI]

BMC Bioinform., 2016

T2: Temporal Property Verification.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Finding Recurrent Sets with Backward Analysis and Trace Partitioning.

[BibT_eX]

[DOI]

Alexey Bakhirkin

Manuela-Luminita Bujorianu

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Safety Verification of Piecewise-Deterministic Markov Processes.

[BibT_eX]

[DOI]

Rafael Wisniewski

Christoffer Sloth

Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, 2016

Static Analysis of Parity Games: Alternating Reachability Under Parity.

[BibT_eX]

[DOI]

Proceedings of the Semantics, Logics, and Calculi, 2016

2015

Timing Semantics for Abstraction and Execution of Synthesized High-Level Robot Control.

[BibT_eX]

[DOI]

IEEE Trans. Robotics, 2015

The Rabin index of parity games: Its complexity and approximation.

[BibT_eX]

[DOI]

Inf. Comput., 2015

Fairness for Infinite-State Systems.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics.

[BibT_eX]

[DOI]

Pablo F. Castro

Cecilia Kilmurray

Proceedings of the 32nd International Symposium on Theoretical Aspects of Computer Science, 2015

A Forward Analysis for Recurrent Sets.

[BibT_eX]

[DOI]

Alexey Bakhirkin

Josh Berdine

Proceedings of the Static Analysis - 22nd International Symposium, 2015

A Recursive Probabilistic Temporal Logic.

[BibT_eX]

[DOI]

Pablo F. Castro

Cecilia Kilmurray

Manuela-Luminita Bujorianu

Proceedings of the Formal Methods and Software Engineering, 2015

A Modelling Framework for Cyber-Physical System Resilience.

[BibT_eX]

[DOI]

Proceedings of the Cyber Physical Systems. Design, Modeling, and Evaluation, 2015

Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

On Automation of CTL* Verification for Infinite-State Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Fatal Attractors in Parity Games: Building Blocks for Partial Solvers.

[BibT_eX]

[DOI]

CoRR, 2014

Backward Analysis via over-Approximate Abstraction and under-Approximate Subtraction.

[BibT_eX]

[DOI]

Alexey Bakhirkin

Josh Berdine

Proceedings of the Static Analysis - 21st International Symposium, 2014

Faster temporal reasoning for infinite-state programs.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Finding Instability in Biological Models.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

Controllability in Partial and Uncertain Environments.

[BibT_eX]

[DOI]

Proceedings of the 14th International Conference on Application of Concurrency to System Design, 2014

2013

Synthesizing nonanomalous event-based controllers for liveness goals.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2013

The Rabin index of parity games.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fourth International Symposium on Games, 2013

Synthesis of biological models from mutation experiments.

[BibT_eX]

[DOI]

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Synthesis from Temporal Specifications: New Applications in Robotics and Model-Driven Development.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2013, 2013

Controller synthesis: from modelling to enactment.

[BibT_eX]

[DOI]

Proceedings of the 35th International Conference on Software Engineering, 2013

Provably correct continuous control for high-level robot behaviors with actions of arbitrary execution durations.

[BibT_eX]

[DOI]

Vasumathi Raman

Hadas Kress-Gazit

Proceedings of the 2013 IEEE International Conference on Robotics and Automation, 2013

Fatal Attractors in Parity Games.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2013

At the interface of biology and computation.

[BibT_eX]

[DOI]

Proceedings of the 2013 ACM SIGCHI Conference on Human Factors in Computing Systems, 2013

Model-Checking Signal Transduction Networks through Decreasing Reachability Sets.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

p-Automata: New foundations for discrete-time probabilistic verification.

[BibT_eX]

[DOI]

Daniel Wagner

Perform. Evaluation, 2012

Synthesis of Reactive(1) designs.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2012

Effective Synthesis of Asynchronous Systems from GR(1) Specifications.

[BibT_eX]

[DOI]

Uri Klein

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Predictive Modelling of Stem Cell Differentiation and Apoptosis in C. elegans.

[BibT_eX]

[DOI]

Antje Beyer

Ralf Eberhard

Michael O. Hengartner

Alex Hajnal

Proceedings of the Information Processign in Cells and Tissues, 2012

The Modal Transition System Control Problem.

[BibT_eX]

[DOI]

Proceedings of the FM 2012: Formal Methods, 2012

Bma: Visual Tool for Modeling and Analyzing Biological Networks.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

LTL generalized model checking revisited.

[BibT_eX]

[DOI]

Patrice Godefroid

Int. J. Softw. Tools Technol. Transf., 2011

Proving Stabilization of Biological Systems.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011

p-Automata and Obligation Games.

[BibT_eX]

[DOI]

Proceedings of the Eighteenth International Symposium on Temporal Representation and Reasoning, 2011

Synthesis of live behaviour models for fallible domains.

[BibT_eX]

[DOI]

Proceedings of the 33rd International Conference on Software Engineering, 2011

The Rabin Index of Parity Games - (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2011

Concurrent Small Progress Measures.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2011

The Only Way Is Up.

[BibT_eX]

[DOI]

Proceedings of the FM 2011: Formal Methods, 2011

Dynamic Reactive Modules.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

2010

PCTL model checking of Markov chains: Truth and falsity as winning strategies in games.

[BibT_eX]

[DOI]

Perform. Evaluation, 2010

Strategy logic.

[BibT_eX]

[DOI]

Inf. Comput., 2010

Synthesis of live behaviour models.

[BibT_eX]

[DOI]

Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010

From Mtl to Deterministic Timed Automata.

[BibT_eX]

[DOI]

Dejan Nickovic

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2010

An Automata-Theoretic Approach to Infinite-State Systems.

[BibT_eX]

[DOI]

Proceedings of the Time for Verification, 2010

2009

From liveness to promptness.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2009

A workbench for preprocessor design and evaluation: toward benchmarks for parity games.

[BibT_eX]

[DOI]

Huaxin Wang

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2009

Computational modeling of the EGFR network elucidates control mechanisms regulating signal dynamics.

[BibT_eX]

[DOI]

BMC Syst. Biol., 2009

Lower Bounds on Witnesses for Nonemptiness of Universal Co-Büchi Automata.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2009

Three-Valued Abstractions of Markov Chains: Completeness for a Sizeable Fragment of PCTL.

[BibT_eX]

[DOI]

Daniel Wagner

Proceedings of the Fundamentals of Computation Theory, 17th International Symposium, 2009

2008

Algorithms for Büchi Games

[BibT_eX]

[DOI]

CoRR, 2008

Hintikka Games for PCTL on Labeled Markov Chains.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Conference on the Quantitative Evaluaiton of Systems (QEST 2008), 2008

Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Systems Biology, First International Workshop, 2008

2007

Predictive Modeling of Signaling Crosstalk during <i>C. elegans</i> Vulval Development.

[BibT_eX]

[DOI]

PLoS Comput. Biol., 2007

From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2007

Specify, Compile, Run: Hardware from PSL.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Compiler Optimization meets Compiler Verification, 2007

Generalized Parity Games.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2007

Interactive presentation: Automatic hardware synthesis from specifications: a case study.

[BibT_eX]

[DOI]

Proceedings of the 2007 Design, Automation and Test in Europe Conference and Exposition, 2007

2006

Liveness with invisible ranking.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2006

Synthesis of Reactive(1) Designs.

[BibT_eX]

[DOI]

Yaniv Sa'ar

Proceedings of the Verification, 2006

Faster Solutions of Rabin and Streett Games.

[BibT_eX]

[DOI]

Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

Solving Games Without Determinization.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 20th International Workshop, 2006

Safraless Compositional Synthesis.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Minimizing Generalized Büchi Automata.

[BibT_eX]

[DOI]

Sudeep Juvekar

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

Inferring Network Invariants Automatically.

[BibT_eX]

[DOI]

Olga Grinchtein

Martin Leucker

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

Bridging the gap between fair simulation and trace inclusion.

[BibT_eX]

[DOI]

Yonit Kesten

Inf. Comput., 2005

2004

SAT-based Induction for Temporal Safety Properties.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Bounded Model Checking, 2004

Liveness with Incomprehensible Ranking.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Combining State-Based and Scenario-Based Approaches in Modeling Biological Systems.

[BibT_eX]

[DOI]

David Harel

E. Jane Albert Hubbard

Michael J. Stern

Naamah Swerdlin

Proceedings of the Computational Methods in Systems Biology, International Conference, 2004

Global Model-Checking of Infinite-State Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

From bidirectionality to alternation.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2003

Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems.

[BibT_eX]

[DOI]

Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

Enhanced Vacuity Detection in Linear Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

Fair Equivalence Relations.

[BibT_eX]

[DOI]

Proceedings of the Verification: Theory and Practice, 2003

2002

Pushdown Specifications.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2002

Model Checking Linear Properties of Prefix-Recognizable Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001

Extended Temporal Logic Revisited.

[BibT_eX]

[DOI]