2024
Distributional Reachability for Markov Decision Processes: Theory and Applications.
IEEE Trans. Autom. Control., July, 2024

Symbolic Task Inference in Deep Reinforcement Learning.
J. Artif. Intell. Res., 2024

Enhancing Data-Driven Stochastic Control via Bundled Interval MDP.
IEEE Control. Syst. Lett., 2024

Temporal-Difference Variational Continual Learning.
CoRR, 2024

A data-driven approach for safety quantification of non-linear stochastic systems with unknown additive noise distribution.
CoRR, 2024

DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications.
CoRR, 2024

Games for AI Control: Models of Safety Evaluations of AI Deployment Protocols.
CoRR, 2024

Networked Communication for Mean-Field Games with Function Approximation and Empirical Mean-Field Estimation.
CoRR, 2024

Learning Provably Robust Policies in Uncertain Parametric Environments.
CoRR, 2024

Walking the Values in Bayesian Inverse Reinforcement Learning.
CoRR, 2024

The Perils of Optimizing Learned Reward Functions: Low Training Error Does Not Guarantee Low Regret.
CoRR, 2024

Deep Bayesian Active Learning for Preference Modeling in Large Language Models.
CoRR, 2024

Data-driven memory-dependent abstractions of dynamical systems via a Cantor-Kantorovich metric.
CoRR, 2024

Distributionally Robust Aggregation of Electric Vehicle Flexibility.
CoRR, 2024

Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems.
CoRR, 2024

Safe Reach Set Computation via Neural Barrier Certificates.
CoRR, 2024

Data-driven Interval MDP for Robust Control Synthesis.
CoRR, 2024

Distributed Markov Chain Monte Carlo Sampling based on the Alternating Direction Method of Multipliers.
CoRR, 2024

Probabilistic reach-avoid for Bayesian neural networks.
Artif. Intell., 2024

Learning robust policies for uncertain parametric Markov decision processes.
Proceedings of the 6th Annual Learning for Dynamics & Control Conference, 2024

Bounded robustness in reinforcement learning via lexicographic objectives.
Proceedings of the 6th Annual Learning for Dynamics & Control Conference, 2024

Learning-based rigid tube model predictive control.
Proceedings of the 6th Annual Learning for Dynamics & Control Conference, 2024

STARC: A General Framework For Quantifying Differences Between Reward Functions.
Proceedings of the Twelfth International Conference on Learning Representations, 2024

Quantifying the Sensitivity of Inverse Reinforcement Learning to Misspecification.
Proceedings of the Twelfth International Conference on Learning Representations, 2024

CTL Model Checking of MDPs over Distribution Spaces: Algorithms and Sampling-based Computations.
Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, 2024

Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models.
Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, 2024

A Stability-Based Abstraction Framework for Reach-Avoid Control of Stochastic Dynamical Systems with Unknown Noise Distributions.
Proceedings of the European Control Conference, 2024

Bisimulation Learning.
Proceedings of the Computer Aided Verification - 36th International Conference, 2024

Stochastic Omega-Regular Verification and Control with Supermartingales.
Proceedings of the Computer Aided Verification - 36th International Conference, 2024

Safeguarded Progress in Reinforcement Learning: Safe Bayesian Exploration for Control Policy Synthesis.
Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

Reasoning about Causality in Games (Abstract Reprint).
Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

Stability Analysis of Switched Linear Systems with Neural Lyapunov Functions.
Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence, 2024

2023
Introduction to the Special Issue on QEST 2021.
ACM Trans. Model. Comput. Simul., October, 2023

Grid-Free Computation of Probabilistic Safety With Malliavin Calculus.
IEEE Trans. Autom. Control., October, 2023

Certified reinforcement learning with logic guidance.
Artif. Intell., September, 2023

Reasoning about causality in games.
Artif. Intell., July, 2023

Synthesising Programs with Non-trivial Constants.
J. Autom. Reason., June, 2023

Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions.
J. Artif. Intell. Res., 2023

Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions.
Proceedings of the Proceedings Fifth International Workshop on Formal Methods for Autonomous Systems, 2023

A General Verification Framework for Dynamical and Control Models via Certificate Synthesis.
CoRR, 2023

Formal Analysis and Verification of Max-Plus Linear Systems.
CoRR, 2023

On Imperfect Recall in Multi-Agent Influence Diagrams.
Proceedings of the Proceedings Nineteenth conference on Theoretical Aspects of Rationality and Knowledge, 2023

Networked Communication for Decentralised Agents in Mean-Field Games.
CoRR, 2023

Model Reduction of Linear Stochastic Systems with Preservation of sc-LTL Specifications.
CoRR, 2023

Robust Tube Model Predictive Control with Uncertainty Quantification for Discrete-Time Linear Systems.
CoRR, 2023

Data-driven abstractions via adaptive refinements and a Kantorovich metric [extended version].
CoRR, 2023

k-Prize Weighted Voting Games.
CoRR, 2023

Quantitative Verification With Neural Networks For Probabilistic Programs and Stochastic Systems.
CoRR, 2023

On the limitations of Markovian rewards to express multi-objective, risk-sensitive, and modal tasks.
Proceedings of the Uncertainty in Artificial Intelligence, 2023

Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics.
Proceedings of the Quantitative Evaluation of Systems - 20th International Conference, 2023

On the Trade-Off Between Efficiency and Precision of Neural Abstraction.
Proceedings of the Quantitative Evaluation of Systems - 20th International Conference, 2023

Policy Evaluation in Distributional LQR.
Proceedings of the Learning for Dynamics and Control Conference, 2023

Data-driven memory-dependent abstractions of dynamical systems.
Proceedings of the Learning for Dynamics and Control Conference, 2023

Invariance in Policy Optimisation and Partial Identifiability in Reward Learning.
Proceedings of the International Conference on Machine Learning, 2023

Learning Task Automata for Reinforcement Learning Using Hidden Markov Models.
Proceedings of the ECAI 2023 - 26th European Conference on Artificial Intelligence, September 30 - October 4, 2023, Kraków, Poland, 2023

Quantitative Verification with Neural Networks.
Proceedings of the 34th International Conference on Concurrency Theory, 2023

Distributionally Robust Optimal and Safe Control of Stochastic Systems via Kernel Conditional Mean Embedding.
Proceedings of the 62nd IEEE Conference on Decision and Control, 2023

An Exact Characterisation of Flexibility in Populations of Electric Vehicles.
Proceedings of the 62nd IEEE Conference on Decision and Control, 2023

Inner Approximations of Stochastic Programs for Data-Driven Stochastic Barrier Function Design.
Proceedings of the 62nd IEEE Conference on Decision and Control, 2023

Abstracting Linear Stochastic Systems via Knowledge Filtering.
Proceedings of the 62nd IEEE Conference on Decision and Control, 2023

Data-driven Abstractions via Adaptive Refinements and a Kantorovich Metric.
Proceedings of the 62nd IEEE Conference on Decision and Control, 2023

k-Prize Weighted Voting Game.
Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems, 2023

ARCH-COMP23 Category Report: Stochastic Models.
Proceedings of 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23), 2023

Misspecification in Inverse Reinforcement Learning.
Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence, 2023

Low Emission Building Control with Zero-Shot Reinforcement Learning.
Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence, 2023

Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty.
Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence, 2023

2022
SMT-Based Reachability Analysis of High Dimensional Interval Max-Plus Linear Systems.
IEEE Trans. Autom. Control., 2022

Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-Time Systems.
IEEE Trans. Autom. Control., 2022

Introduction to the Special Issue on Distributed Hybrid Systems.
Leibniz Trans. Embed. Syst., 2022

Hierarchical identification of nonlinear hybrid systems in a Bayesian framework.
Inf. Comput., 2022

Special issue: Formal verification of cyber-physical systems.
Inf. Comput., 2022

Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics.
CoRR, 2022

Observational Robustness and Invariances in Reinforcement Learning via Lexicographic Objectives.
CoRR, 2022

LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning.
CoRR, 2022

Automated verification and synthesis of stochastic hybrid systems: A survey.
Autom., 2022

LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning.
Proceedings of the Quantitative Evaluation of Systems - 19th International Conference, 2022

Neural Abstractions.
Proceedings of the Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, 2022

Lexicographic Multi-Objective Reinforcement Learning.
Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022

ARCH-COMP22 Category Report: Stochastic Models.
Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22), 2022

Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise.
Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence, 2022

2021
Modular Deep Reinforcement Learning for Continuous Motion Planning With Temporal Logic.
IEEE Robotics Autom. Lett., October, 2021

Aggregation and Control of a Heterogeneous Population of Solar Panels Over the Grid Frequency.
IEEE Trans. Control. Syst. Technol., 2021

Formal and Efficient Synthesis for Continuous-Time Linear Stochastic Hybrid Processes.
IEEE Trans. Autom. Control., 2021

Formal Control Synthesis via Simulation Relations and Behavioral Theory for Discrete-Time Descriptor Systems.
IEEE Trans. Autom. Control., 2021

Adaptive formal approximations of Markov chains.
Perform. Evaluation, 2021

Resilient monitoring in self-adaptive systems through behavioral parameter estimation.
J. Syst. Archit., 2021

Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration.
J. Autom. Reason., 2021

Formal Synthesis of Lyapunov Neural Networks.
IEEE Control. Syst. Lett., 2021

Rational verification: game-theoretic verification of multi-agent systems.
Appl. Intell., 2021

Certification of iterative predictions in Bayesian neural networks.
Proceedings of the Thirty-Seventh Conference on Uncertainty in Artificial Intelligence, 2021

Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

QUILT: quantify, infer and label the thermal efficiency of heating and cooling residential homes.
Proceedings of the BuildSys '21: The 8th ACM International Conference on Systems for Energy-Efficient Buildings, Cities, and Transportation, Coimbra, Portugal, November 17, 2021

PyCID: A Python Library for Causal Influence Diagrams.
Proceedings of the 20th Python in Science Conference 2021 (SciPy 2021), Virtual Conference, July 12, 2021

FOSSIL: a software tool for the formal synthesis of lyapunov functions and barrier certificates using neural networks.
Proceedings of the HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control, 2021

A Software Tool for the Formal Synthesis of Lyapunov Functions and Barrier Certificates using Neural Networks.
Proceedings of the 3rd Workshop on Artificial Intelligence and Formal Verification, 2021

Formal Abstraction and Synthesis of Parametric Stochastic Processes.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2021

SMT-Based Model Checking of Max-Plus Linear Systems.
Proceedings of the 32nd International Conference on Concurrency Theory, 2021

Learning Probabilistic Termination Proofs.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Equilibrium Refinements for Multi-Agent Influence Diagrams: Theory and Practice.
Proceedings of the AAMAS '21: 20th International Conference on Autonomous Agents and Multiagent Systems, 2021

Multi-Agent Reinforcement Learning with Temporal Logic Specifications.
Proceedings of the AAMAS '21: 20th International Conference on Autonomous Agents and Multiagent Systems, 2021

ARCH-COMP21 Category Report: Stochastic Models.
Proceedings of the 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), 2021

A Bayesian Framework for Large-Scale Identification of Nonlinear Hybrid Systems.
Proceedings of the 7th IFAC Conference on Analysis and Design of Hybrid Systems, 2021

DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning.
Proceedings of the Thirty-Fifth AAAI Conference on Artificial Intelligence, 2021

2020
Symbolic Reachability Analysis of High Dimensional Max-Plus Linear Systems.
CoRR, 2020

Automated Formal Synthesis of Neural Barrier Certificates for Dynamical Models.
CoRR, 2020

Jump Operator Planning: Goal-Conditioned Policy Ensembles and Zero-Shot Transfer.
CoRR, 2020

Acceleration of Descent-based Optimization Algorithms via Carathéodory's Theorem.
CoRR, 2020

Automated Formal Synthesis of Lyapunov Neural Networks.
CoRR, 2020

Automated formal synthesis of provably safe digital controllers for continuous plants.
Acta Informatica, 2020

Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

SMITE: Using Smart Meters to Infer the Thermal Efficiency of Residential Homes.
Proceedings of the BuildSys '20: The 7th ACM International Conference on Systems for Energy-Efficient Buildings, 2020

SafePILCO: A Software Tool for Safe and Data-Efficient Policy Synthesis.
Proceedings of the Quantitative Evaluation of Systems - 17th International Conference, 2020

A Randomized Algorithm to Reduce the Support of Discrete Measures.
Proceedings of the Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, 2020

Deep Reinforcement Learning with Temporal Logics.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2020

Computation of the Transient in Max-Plus Linear Systems via SMT-Solving.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2020

ABC(SMC)<sup>2</sup>: Simultaneous Inference and Model Checking of Chemical Reaction Networks.
Proceedings of the Computational Methods in Systems Biology, 2020

Safety Guarantees for Iterative Predictions with Gaussian Processes.
Proceedings of the 59th IEEE Conference on Decision and Control, 2020

Cautious Reinforcement Learning with Logical Constraints.
Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems, 2020

ARCH-COMP20 Category Report: Hybrid Systems with Piecewise Constant Dynamics and Bounded Model Checking.
Proceedings of the ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), 2020

ARCH-COMP20 Category Report: Stochastic Models.
Proceedings of the ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), 2020

2019
Safety Guarantees for Planning Based on Iterative Gaussian Processes.
CoRR, 2019

DeepSynth: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning.
CoRR, 2019

Modular Deep Reinforcement Learning with Temporal Logic Specifications.
CoRR, 2019

Verifying Reachability Properties in Markov Chains via Incremental Induction.
CoRR, 2019

Analyzing Occupancy-Driven Thermal Dynamics in Smart Buildings.
CoRR, 2019

Linear quadratic regulation of polytopic time-inhomogeneous Markov jump linear systems (extended version).
CoRR, 2019

Certified Reinforcement Learning with Logic Guidance.
CoRR, 2019

StocHy: automated verification and synthesis of stochastic processes.
CoRR, 2019

\mathsf StocHy : Automated Verification and Synthesis of Stochastic Processes.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Bayes-Adaptive Planning for Data-Efficient Verification of Uncertain Markov Decision Processes.
Proceedings of the Quantitative Evaluation of Systems, 16th International Conference, 2019

Safety Guarantees for the Electricity Grid with Significant Renewables Generation.
Proceedings of the Quantitative Evaluation of Systems, 16th International Conference, 2019

Efficiency through uncertainty: scalable formal synthesis for stochastic hybrid systems.
Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019

StocHy - automated verification and synthesis of stochastic processes: poster abstract.
Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, 2019

Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2019

Bayesian Verification of Chemical Reaction Networks.
Proceedings of the Formal Methods. FM 2019 International Workshops, 2019

Linear quadratic regulation of polytopic time-inhomogeneous Markov jump linear systems.
Proceedings of the 17th European Control Conference, 2019

ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics.
Proceedings of the ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systemsi, 2019

ARCH-COMP19 Category Report: Stochastic Modelling.
Proceedings of the ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systemsi, 2019

Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees.
Proceedings of the 58th IEEE Conference on Decision and Control, 2019

Safe Policy Search Using Gaussian Process Models.
Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, 2019

Logically-Constrained Neural Fitted Q-iteration.
Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, 2019

Towards Verifiable and Safe Model-Free Reinforcement Learning.
Proceedings of the 1st Workshop on Artificial Intelligence and Formal Verification, 2019

2018
Maintenance of Smart Buildings using Fault Trees.
ACM Trans. Sens. Networks, 2018

Multiobjective Optimal Control With Safety as a Priority.
IEEE Trans. Control. Syst. Technol., 2018

Symbolic Abstractions of Networked Control Systems.
IEEE Trans. Control. Netw. Syst., 2018

Approximate Abstractions of Markov Chains with Interval Decision Processes (Extended Version).
CoRR, 2018

Benchmarks for cyber-physical systems: A modular model library for building automation systems (Extended version).
CoRR, 2018

Logically-Correct Reinforcement Learning.
CoRR, 2018

Tropical Abstractions of Max-Plus Linear Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2018

Modelling Smart Buildings Using Fault Maintenance Trees.
Proceedings of the Computer Performance Engineering - 15th European Workshop, 2018

Experimental Biological Protocols with Formal Semantics.
Proceedings of the Computational Methods in Systems Biology, 2018

Impact of Solar Panels and Cooling Devices on Frequency Control After a Generation Loss Incident.
Proceedings of the 57th IEEE Conference on Decision and Control, 2018

Counterexample Guided Inductive Synthesis Modulo Theories.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Approximate Abstractions of Markov Chains with Interval Decision Processes.
Proceedings of the 6th IFAC Conference on Analysis and Design of Hybrid Systems, 2018

Temporal logic control of general Markov decision processes by approximate policy refinement.
Proceedings of the 6th IFAC Conference on Analysis and Design of Hybrid Systems, 2018

ARCH-COMP18 Category Report: Hybrid Systems with Piecewise Constant Dynamics.
Proceedings of the ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, 2018

Benchmarks for stochastic models from building automation systems.
Proceedings of the ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, 2018

Benchmarks for cyber-physical systems: A modular model library for building automation systems.
Proceedings of the 6th IFAC Conference on Analysis and Design of Hybrid Systems, 2018

ARCH-COMP18 Category Report: Stochastic Modelling.
Proceedings of the ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, 2018

2017
Verification of General Markov Decision Processes by Approximate Similarity Relations and Policy Refinement.
SIAM J. Control. Optim., 2017

Certified policy synthesis for general Markov decision processes: An application in building automation systems.
Perform. Evaluation, 2017

Quantitative model-checking of controlled discrete-time Markov processes.
Inf. Comput., 2017

Towards scalable synthesis of stochastic control systems.
Discret. Event Dyn. Syst., 2017

Safe Policy Search with Gaussian Process Models.
CoRR, 2017

Control refinement for discrete-time descriptor systems: a behavioural approach via simulation relations.
CoRR, 2017

On the Relationship between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context (Extended Version).
CoRR, 2017

Data-driven and model-based verification via Bayesian identification and reachability analysis.
Autom., 2017

Dynamic Bayesian networks for formal verification of structured stochastic processes.
Acta Informatica, 2017

Efficient probabilistic model checking of smart building maintenance using fault maintenance trees.
Proceedings of the 4th ACM International Conference on Systems for Energy-Efficient Built Environments, 2017

Automated Experiment Design for Data-Efficient Verification of Parametric Markov Decision Processes.
Proceedings of the Quantitative Evaluation of Systems - 14th International Conference, 2017

Aggregated Markov Models of a Heterogeneous Population of Photovoltaic Panels.
Proceedings of the Quantitative Evaluation of Systems - 14th International Conference, 2017

Formal verification of complex systems: model-based and data-driven methods.
Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, 2017

DSSynth: an automated digital controller synthesis tool for physical plants.
Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

Multi-objective optimal control with safety as a priority.
Proceedings of the 8th International Conference on Cyber-Physical Systems, 2017

Reachability Computation for Switching Diffusions: Finite Abstractions with Certifiable and Tuneable Precision.
Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants.
Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, 2017

On the Relationship Between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context.
Proceedings of the Foundations of Software Science and Computation Structures, 2017

ARCH-COMP17 Category Report: Hybrid Systems with Piecewise Constant Dynamics.
Proceedings of the ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, 2017

Optimal robust control and a separation principle for polytopic time-inhomogeneous Markov jump linear systems.
Proceedings of the 56th IEEE Annual Conference on Decision and Control, 2017

Sound Numerical Computations in Abstract Acceleration.
Proceedings of the Numerical Software Verification - 10th International Workshop, 2017

Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016
Formal Verification of Stochastic Max-Plus-Linear Systems.
IEEE Trans. Autom. Control., 2016

VeriSiMPL 2: An open-source software for the verification of max-plus-linear systems.
Discret. Event Dyn. Syst., 2016

Safety Verification of Continuous-Space Pure Jump Markov Processes.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Formal and Data Association Aware Robust Belief Space Planning.
Proceedings of the STAIRS 2016, 2016

Data-Efficient Bayesian Verification of Parametric Markov Chains.
Proceedings of the Quantitative Evaluation of Systems - 13th International Conference, 2016

Verification of General Markov Decision Processes by Approximate Similarity Relations and Policy Refinement.
Proceedings of the Quantitative Evaluation of Systems - 13th International Conference, 2016

Safety verification of output feedback controllers for nonlinear systems.
Proceedings of the 15th European Control Conference, 2016

Efficient HVAC controls: A symbolic approach.
Proceedings of the 15th European Control Conference, 2016

Experiment design for formal verification via stochastic optimal control.
Proceedings of the 15th European Control Conference, 2016

Verification of Networks of Smart Energy Systems over the Cloud.
Proceedings of the Numerical Software Verification - 9th International Workshop, 2016

Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations.
Proceedings of the Automated Technology for Verification and Analysis, 2016

2015
Aggregation and Control of Populations of Thermostatically Controlled Loads by Formal Abstractions.
IEEE Trans. Control. Syst. Technol., 2015

Quantitative Approximation of the Probability Distribution of a Markov Process by Formal Abstractions.
Log. Methods Comput. Sci., 2015

Observer-based correct-by-design controller synthesis.
CoRR, 2015

Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration (extended version).
CoRR, 2015

Symbolic models for stochastic switched systems: A discretization and a discretization-free approach.
Autom., 2015

Computational techniques for reachability analysis of Max-Plus-Linear systems.
Autom., 2015

FAUST <sup> 2</sup> : Formal Abstractions of Uncountable-STate STochastic Processes.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration.
Proceedings of the Static Analysis - 22nd International Symposium, 2015

Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2015

Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes.
Proceedings of the 26th International Conference on Concurrency Theory, 2015

Data-driven and model-based verification: A Bayesian identification approach.
Proceedings of the 54th IEEE Conference on Decision and Control, 2015

Correct-by-design output feedback of LTI systems.
Proceedings of the 54th IEEE Conference on Decision and Control, 2015

Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Data-driven property verification of grey-box systems by Bayesian experiment design.
Proceedings of the American Control Conference, 2015

A mean field equilibrium for a model of interbank lending.
Proceedings of the American Control Conference, 2015

Controller Synthesis for Probabilistic Safety Specifications using Observers.
Proceedings of the 5th IFAC Conference on Analysis and Design of Hybrid Systems, 2015

2014
Characterization and computation of infinite-horizon specifications over Markov processes.
Theor. Comput. Sci., 2014

On the Optimal Solutions of the Infinite-Horizon Linear Sensor Scheduling Problem.
IEEE Trans. Autom. Control., 2014

Symbolic Control of Stochastic Systems via Approximately Bisimilar Finite Abstractions.
IEEE Trans. Autom. Control., 2014

Probabilistic Reach-Avoid Computation for Partially Degenerate Stochastic Processes.
IEEE Trans. Autom. Control., 2014

Approximately bisimilar symbolic models for randomly switched stochastic systems.
Syst. Control. Lett., 2014

Modeling, Verification, and Control of Complex Systems for Energy Networks (Dagstuhl Seminar 14441).
Dagstuhl Reports, 2014

Symbolic Models for Networked Control Systems.
CoRR, 2014

Sampling-based Approximations with Quantitative Performance for the Probabilistic Reach-Avoid Problem over General Markov Processes.
CoRR, 2014

Backward Reachability of Autonomous Max-Plus-Linear Systems.
Proceedings of the 12th International Workshop on Discrete Event Systems, 2014

Precise Approximations of the Probability Distribution of a Markov Process in Time: An Application to Probabilistic Invariance.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Forward Reachability Computation for Autonomous Max-Plus-Linear Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Formal Synthesis and Validation of Inhomogeneous Thermostatically Controlled Loads.
Proceedings of the Quantitative Evaluation of Systems - 11th International Conference, 2014

Finite Abstractions of Stochastic Max-Plus-Linear Systems.
Proceedings of the Quantitative Evaluation of Systems - 11th International Conference, 2014

Bisimilar symbolic models for stochastic control systems without state-space discretization.
Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 2014

On approximation metrics for linear temporal model-checking of stochastic systems.
Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 2014

Towards Real-Time Control of Gene Expression at the Single Cell Level: A Stochastic Control Approach.
Proceedings of the Computational Methods in Systems Biology, 2014

Finite abstractions of networked control systems.
Proceedings of the 53rd IEEE Conference on Decision and Control, 2014

Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations.
Proceedings of the Horizons of the Mind. A Tribute to Prakash Panangaden, 2014

Symbolic models for randomly switched stochastic systems.
Proceedings of the American Control Conference, 2014

2013
Finite Abstractions of Max-Plus-Linear Systems.
IEEE Trans. Autom. Control., 2013

Adaptive and Sequential Gridding Procedures for the Abstraction and Verification of Stochastic Processes.
SIAM J. Appl. Dyn. Syst., 2013

A stochastic games framework for verification and control of discrete time stochastic hybrid systems.
Autom., 2013

Symbolic Control of Stochastic Switched Systems via Finite Abstractions.
Proceedings of the Quantitative Evaluation of Systems - 10th International Conference, 2013

VeriSiMPL: Verification via biSimulations of MPL Models.
Proceedings of the Quantitative Evaluation of Systems - 10th International Conference, 2013

Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems.
Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013

Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems.
Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013

Symbolic models for stochastic control systems without stability assumptions.
Proceedings of the 12th European Control Conference, 2013

Aggregation of thermostatically controlled loads by formal abstractions.
Proceedings of the 12th European Control Conference, 2013

Bisimilar finite abstractions of stochastic control systems.
Proceedings of the 52nd IEEE Conference on Decision and Control, 2013

A control Lyapunov function approach for the computation of the infinite-horizon stochastic reach-avoid problem.
Proceedings of the 52nd IEEE Conference on Decision and Control, 2013

Optimal control of partially observable discrete time stochastic hybrid systems for safety specifications.
Proceedings of the American Control Conference, 2013

Finite abstractions of nonautonomous Max-Plus-Linear systems.
Proceedings of the American Control Conference, 2013

2012
A Mathematical Model to Study the Dynamics of Epithelial Cellular Networks.
IEEE ACM Trans. Comput. Biol. Bioinform., 2012

Infinite-Horizon Switched LQR Problems in Discrete Time: A Suboptimal Algorithm With Performance Analysis.
IEEE Trans. Autom. Control., 2012

On infinite horizon switched LQR problems with state and control constraints.
Syst. Control. Lett., 2012

On efficient sensor scheduling for linear dynamical systems.
Autom., 2012

Modeling and simulation of a microgrid as a Stochastic Hybrid System.
Proceedings of the 3rd IEEE PES Innovative Smart Grid Technologies Europe, 2012

Regularization of bellman equations for infinite-horizon probabilistic properties.
Proceedings of the Hybrid Systems: Computation and Control (part of CPS Week 2012), 2012

Probabilistic invariance of mixed deterministic-stochastic dynamical systems.
Proceedings of the Hybrid Systems: Computation and Control (part of CPS Week 2012), 2012

Robust PCTL model checking.
Proceedings of the Hybrid Systems: Computation and Control (part of CPS Week 2012), 2012

Stability and attractivity of absorbing sets for discrete-time Markov processes.
Proceedings of the 51th IEEE Conference on Decision and Control, 2012

Higher-Order Approximations for Verification of Stochastic Hybrid Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2012

Abstraction and verification of autonomous Max-Plus-Linear systems.
Proceedings of the American Control Conference, 2012

2011
Approximate Abstractions of Stochastic Hybrid Systems.
IEEE Trans. Autom. Control., 2011

Versatile spectral methods for point set matching.
Pattern Recognit. Lett., 2011

Approximation Metrics Based on Probabilistic Bisimulations for General State-Space Markov Processes: A Survey.
Proceedings of the First Workshop on Hybrid Autonomous Systems, 2011

Adaptive Gridding for Abstraction and Verification of Stochastic Hybrid Systems.
Proceedings of the Eighth International Conference on Quantitative Evaluation of Systems, 2011

Quantitative automata model checking of autonomous stochastic hybrid systems.
Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, 2011

On infinite-horizon probabilistic properties and stochastic bisimulation functions.
Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference, 2011

Discrete time stochastic hybrid dynamical games: Verification & controller synthesis.
Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference, 2011

Approximate abstractions of stochastic systems: A randomized method.
Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference, 2011

2010
Probabilistic safety and optimal control for survival analysis of Bacillus subtilis.
Syst. Control. Lett., 2010

Approximate Model Checking of Stochastic Hybrid Systems.
Eur. J. Control, 2010

On the optimal solutions of the infinite-horizon linear sensor scheduling problem.
Proceedings of the 49th IEEE Conference on Decision and Control, 2010

On sensor scheduling of linear dynamical systems with error bounds.
Proceedings of the 49th IEEE Conference on Decision and Control, 2010

On the infinite horizon constrained switched LQR problem.
Proceedings of the 49th IEEE Conference on Decision and Control, 2010

Probabilistic bisimulations of switching and resetting diffusions.
Proceedings of the 49th IEEE Conference on Decision and Control, 2010

2009
On the Value Functions of the Discrete-Time Switched LQR Problem.
IEEE Trans. Autom. Control., 2009

Exponential stabilization of discrete-time switched linear systems.
Autom., 2009

Box invariance in biologically-inspired dynamical systems.
Autom., 2009

The Emergent Structure of the Drosophila Wing - A Dynamic Model Generator.
Proceedings of the VISAPP 2009 - Proceedings of the Fourth International Conference on Computer Vision Theory and Applications, Lisboa, Portugal, February 5-8, 2009, 2009

Stabilization of Discrete-Time Switched Linear Systems: A Control-Lyapunov Function Approach.
Proceedings of the Hybrid Systems: Computation and Control, 12th International Conference, 2009

On piecewise quadratic control-Lyapunov functions for switched linear systems.
Proceedings of the 48th IEEE Conference on Decision and Control, 2009

A contractivity approach for probabilistic bisimulations of diffusion processes.
Proceedings of the 48th IEEE Conference on Decision and Control, 2009

Efficient suboptimal solutions of switched LQR problems.
Proceedings of the American Control Conference, 2009

2008
Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems.
Autom., 2008

Approximation of General Stochastic Hybrid Systems by Switching Diffusions with Random Hybrid Jumps.
Proceedings of the Hybrid Systems: Computation and Control, 11th International Workshop, 2008

Markov Set-Chains as Abstractions of Stochastic Hybrid Systems.
Proceedings of the Hybrid Systems: Computation and Control, 11th International Workshop, 2008

Approximate abstractions of discrete-time controlled stochastic hybrid systems.
Proceedings of the 47th IEEE Conference on Decision and Control, 2008

An approximate dynamic programming approach to probabilistic reachability for stochastic hybrid systems.
Proceedings of the 47th IEEE Conference on Decision and Control, 2008

2007
The Concept of Deadlock and Livelock in Hybrid Control Systems.
Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

Computational Approaches to Reachability Analysis of Stochastic Hybrid Systems.
Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

Sufficient conditions for the existence of zeno behavior in a class of nonlinear hybrid systems via constant approximations.
Proceedings of the 46th IEEE Conference on Decision and Control, 2007

Quantitative and Probabilistic Modeling in Pathway Logic.
Proceedings of the 7th IEEE International Conference on Bioinformatics and Bioengineering, 2007

2006
Reachability Analysis for Controlled Discrete Time Stochastic Hybrid Systems.
Proceedings of the Hybrid Systems: Computation and Control, 9th International Workshop, 2006

Probabilistic reachability and safe sets computation for discrete time stochastic hybrid systems.
Proceedings of the 45th IEEE Conference on Decision and Control, 2006

Error bounds based stochastic approximations and simulations of hybrid dynamical systems.
Proceedings of the American Control Conference, 2006

A priori detection of Zeno behavior in communication networks modeled as hybrid systems.
Proceedings of the American Control Conference, 2006

Box invariance of Hybrid and switched Systems.
Proceedings of the 2nd IFAC Conference on Analysis and Design of Hybrid Systems, 2006

2005
Sufficient Conditions for the Existence of Zeno Behavior.
Proceedings of the 44th IEEE IEEE Conference on Decision and Control and 8th European Control Conference Control, 2005

Stochastic approximations of hybrid systems.
Proceedings of the American Control Conference, 2005

2004
Optimal control for a class of stochastic hybrid systems.
Proceedings of the 43rd IEEE Conference on Decision and Control, 2004

Robust model predictive control through adjustable variables: an application to path planning.
Proceedings of the 43rd IEEE Conference on Decision and Control, 2004