Davide Bresolin

Massimiliano de Leoni

Aurelo Makaj

Data Knowl. Eng., 2025

2024

A computable and compositional semantics for hybrid systems.

[BibT_eX]

[DOI]

Inf. Comput., 2024

Automated Synthesis of Certified Neural Networks: Initial Results and Open Research Lines.

[BibT_eX]

[DOI]

Nicolò Navarin

Proceedings of the Short Paper Proceedings of the 6th International Workshop on Artificial Intelligence and Formal Verification, 2024

Model Checking of Optimal LTL and ASAP Properties.

[BibT_eX]

[DOI]

Filippo Fantinato

Stefano Tonetta

Proceedings of the Short Paper Proceedings of the 6th International Workshop on Artificial Intelligence and Formal Verification, 2024

Recent Results on Computable and Compositional Semantics for Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Short Paper Proceedings of the 6th International Workshop on Artificial Intelligence and Formal Verification, 2024

Automated Synthesis of Certified Neural Networks.

[BibT_eX]

[DOI]

Nicolò Navarin

Proceedings of the ECAI 2024 - 27th European Conference on Artificial Intelligence, 19-24 October 2024, Santiago de Compostela, Spain, 2024

2023

Supervisory control of business processes with resources, parallel and mutually exclusive branches, loops, and uncertainty.

[BibT_eX]

[DOI]

Inf. Syst., October, 2023

Rigorous Function Calculi in Ariadne.

[BibT_eX]

[DOI]

Pieter Collins

CoRR, 2023

Repair of Unsound Data-Aware Process Models.

[BibT_eX]

[DOI]

Massimiliano de Leoni

Proceedings of the Business Process Management Workshops, 2023

2022

Special issue: Selected papers of the 11th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2020).

[BibT_eX]

[DOI]

Jean-François Raskin

Inf. Comput., 2022

Automating Numerical Parameters Along the Evolution of a Nonlinear System.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification - 22nd International Conference, 2022

Dynamic Controllability of Temporal Networks via Supervisory Control.

[BibT_eX]

[DOI]

Proceedings of the Short Paper Proceedings of the 4th Workshop on Artificial Intelligence and Formal Verification, 2022

2021

Static and dynamic property-preserving updates.

[BibT_eX]

[DOI]

Ivan Lanese

Inf. Comput., 2021

Equivalence checking and intersection of deterministic timed finite state machines.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2021

2020

Higher Order Method for Differential Inclusions.

[BibT_eX]

[DOI]

CoRR, 2020

A computable and compositional semantics for hybrid automata.

[BibT_eX]

[DOI]

Proceedings of the HSCC '20: 23rd ACM International Conference on Hybrid Systems: Computation and Control, 2020

2019

Decidability and complexity of the fragments of the modal logic of Allen's relations over the rationals.

[BibT_eX]

[DOI]

Inf. Comput., 2019

Rigorous Continuous Evolution of Uncertain Systems.

[BibT_eX]

[DOI]

Pieter Collins

Proceedings of the Numerical Software Verification - 12th International Workshop, 2019

Automated Verification of Noisy Nonlinear Cyber-Physical Systems with Ariadne.

[BibT_eX]

[DOI]

Proceedings of the 1st Workshop on Artificial Intelligence and Formal Verification, 2019

2018

Formal Verification of Medical CPS: A Laser Incision Case Study.

[BibT_eX]

[DOI]

ACM Trans. Cyber Phys. Syst., 2018

On Sub-Propositional Fragments of Modal Logic.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2018

Extracting Interval Temporal Logic Rules: A First Approach.

[BibT_eX]

[DOI]

Proceedings of the 25th International Symposium on Temporal Representation and Reasoning, 2018

2017

Horn Fragments of the Halpern-Shoham Interval Temporal Logic.

[BibT_eX]

[DOI]

Michael Zakharyaschev

ACM Trans. Comput. Log., 2017

Finite Satisfiability of Interval Temporal Logic Formulas with Multi-Objective Metaheuristics.

[BibT_eX]

[DOI]

J. Multiple Valued Log. Soft Comput., 2017

Ongoing Work on Automated Verification of Noisy Nonlinear Systems with Ariadne.

[BibT_eX]

[DOI]

Pieter Collins

Proceedings of the Testing Software and Systems, 2017

Most General Property-Preserving Updates.

[BibT_eX]

[DOI]

Ivan Lanese

Proceedings of the Language and Automata Theory and Applications, 2017

Fast(er) Reasoning in Interval Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the 26th EACSL Annual Conference on Computer Science Logic, 2017

2016

On the Expressive Power of Sub-Propositional Fragments of Modal Logic.

[BibT_eX]

[DOI]

Proceedings of the Seventh International Symposium on Games, 2016

Horn Fragments of the Halpern-Shoham Interval Temporal Logic (Technical Report).

[BibT_eX]

[DOI]

Michael Zakharyaschev

CoRR, 2016

Special issue: selected papers from the 21st international symposium on temporal representations and reasoning (TIME-2014).

[BibT_eX]

[DOI]

Acta Informatica, 2016

On the Complexity of Fragments of Horn Modal Logics.

[BibT_eX]

[DOI]

Alberto L. Sangiovanni-Vincentelli

Proceedings of the 23rd International Symposium on Temporal Representation and Reasoning, 2016

2015

A Platform-Based Design Methodology With Contracts and Related Tools for the Design of Cyber-Physical Systems.

[BibT_eX]

[DOI]

Pierluigi Nuzzo

Proc. IEEE, 2015

Formal verification of robotic surgery tasks by reachability analysis.

[BibT_eX]

[DOI]

Microprocess. Microsystems, 2015

On the Complexity of Fragments of the Modal Logic of Allen's Relations over Dense Structures.

[BibT_eX]

[DOI]

Proceedings of the Language and Automata Theory and Applications, 2015

2014

Interval temporal logics over strongly discrete linear orders: Expressiveness and complexity.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2014

Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fifth International Symposium on Games, 2014

The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2014

The dark side of interval temporal logic: marking the undecidability border.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2014

Sub-propositional Fragments of the Interval Temporal Logic of Allen's Relations.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence - 14th European Conference, 2014

Application of contract-based verification techniques for hybrid automata to surgical robotic systems.

[BibT_eX]

[DOI]

Proceedings of the 13th European Control Conference, 2014

DL-Lite and Interval Temporal Logics: a Marriage Proposal.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic, 2014

Verification of Robotic Surgery Tasks by Reachability Analysis: A Comparison of Tools.

[BibT_eX]

[DOI]

Proceedings of the 17th Euromicro Conference on Digital System Design, 2014

A First Study of the Horn Fragment of the Modal Logic of Time Intervals.

[BibT_eX]

[DOI]

Proceedings of the 29th Italian Conference on Computational Logic, 2014

2013

Optimal decision procedures for MPNL over finite structures, the natural numbers, and the integers.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2013

A game-theoretic approach to fault diagnosis and identification of hybrid systems.

[BibT_eX]

[DOI]

Marta Capiluppi

Theor. Comput. Sci., 2013

Metric propositional neighborhood logics on natural numbers.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2013

HyLTL: a temporal logic for model checking hybrid systems.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Third International Workshop on Hybrid Autonomous Systems, 2013

Improving HyLTL model checking of hybrid systems.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fourth International Symposium on Games, 2013

A Tableau System for Right Propositional Neighborhood Logic over Finite Linear Orders: An Implementation.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2013

Finite satisfiability of propositional interval logic formulas with multi-objective evolutionary algorithms.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Genetic Algorithms XII, 2013

2012

On Begins, Meets and before.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 2012

Interval Temporal Logics over Strongly Discrete Linear Orders: the Complete Picture

[BibT_eX]

[DOI]

Proceedings of the Proceedings Third International Symposium on Games, 2012

Ariadne: Dominance Checking of Nonlinear Hybrid Automata Using Reachability Analysis.

[BibT_eX]

[DOI]

Proceedings of the Reachability Problems - 6th International Workshop, 2012

Interval Temporal Logics over Finite Linear Orders: the Complete Picture.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2012, 2012

Open Problems in Verification and Refinement of Autonomous Robotic Systems.

[BibT_eX]

[DOI]

Proceedings of the 15th Euromicro Conference on Digital System Design, 2012

Computing the Evolution of Hybrid Systems using Rigorous Function Calculus.

[BibT_eX]

[DOI]

Proceedings of the 4th IFAC Conference on Analysis and Design of Hybrid Systems, 2012

2011

Robotic Surgery.

[BibT_eX]

[DOI]

IEEE Robotics Autom. Mag., 2011

A Game-Theoretic approach to Fault Diagnosis of Hybrid Systems

[BibT_eX]

[DOI]

Marta Capiluppi

Proceedings of Second International Symposium on Games, 2011

An Optimal Decision Procedure for MPNL over the Integers

[BibT_eX]

[DOI]

Proceedings of Second International Symposium on Games, 2011

The Light Side of Interval Temporal Logic: The Bernays-Schönfinkel's Fragment of CDT.

[BibT_eX]

[DOI]

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

The Dark Side of Interval Temporal Logic: Sharpening the Undecidability Border.

[BibT_eX]

[DOI]

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

Optimal Tableau Systems for Propositional Neighborhood Logic over All, Dense, and Discrete Linear Orders.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2011

What's Decidable about Halpern and Shoham's Interval Logic? The Maximal Fragment ABBL.

[BibT_eX]

[DOI]

Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, 2011

Correct-by-construction code generation from hybrid automata specification.

[BibT_eX]

[DOI]

Proceedings of the 7th International Wireless Communications and Mobile Computing Conference, 2011

2010

Tableaux for Logics of Subinterval Structures over Dense Orderings.

[BibT_eX]

[DOI]

J. Log. Comput., 2010

Begin, After, and Later: a Maximal Decidable Interval Temporal Logic

[BibT_eX]

[DOI]

Proceedings of the Proceedings First Symposium on Games, 2010

A Decidable Spatial Generalization of Metric Interval Temporal Logic.

[BibT_eX]

[DOI]

Proceedings of the TIME 2010, 2010

Metric Propositional Neighborhood Logics: Expressiveness, Decidability, and Undecidability.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2010, 2010

2009

Undecidability of the Logic of Overlap Relation over Discrete Linear Orderings.

[BibT_eX]

[DOI]

Proceedings of the 6th Workshop on Methods for Modalities, 2009

Propositional interval neighborhood logics: Expressiveness, decidability, and undecidable extensions.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2009

A theory of ultimately periodic languages and automata with an application to time granularity.

[BibT_eX]

[DOI]

Gabriele Puppis

Acta Informatica, 2009

Undecidability of Interval Temporal Logics with the Overlap Modality.

[BibT_eX]

[DOI]

Proceedings of the TIME 2009, 2009

A Tableau-Based System for Spatial Reasoning about Directional Relations.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2009

Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths.

[BibT_eX]

[DOI]

Proceedings of the Seventh IEEE International Conference on Software Engineering and Formal Methods, 2009

The impact of EFSM composition on functional ATPG.

[BibT_eX]

[DOI]

Giuseppe Di Guglielmo

Franco Fummi

Graziano Pravadelli

Proceedings of the 2009 IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems, 2009

2008

An optimal tableau for Right Propositional Neighborhood Logic over Trees.

[BibT_eX]

[DOI]

Proceedings of the 15th International Symposium on Temporal Representation and Reasoning, 2008

Decidable and Undecidable Fragments of Halpern and Shoham's Interval Temporal Logic: Towards a Complete Classification.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2008

Optimal Tableaux for Right Propositional Neighborhood Logic over Linear Orders.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence, 11th European Conference, 2008

2007

Proof methods for interval temporal logics.

[BibT_eX]

[DOI]

PhD thesis, 2007

An Optimal Decision Procedure for Right Propositional Neighborhood Logic.

[BibT_eX]

[DOI]

J. Autom. Reason., 2007

Complete and Terminating Tableau for the Logic of Proper Subinterval Structures Over Dense Orderings.

[BibT_eX]

[DOI]

Proceedings of the 5th Workshop on Methods for Modalities, 2007

Tableau Systems for Logics of Subinterval Structures over Dense Orderings.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2007

An Optimal Tableau-Based Decision Algorithm for Propositional Neighborhood Logic.

[BibT_eX]

[DOI]

Proceedings of the STACS 2007, 2007

On Decidability and Expressiveness of Propositional Interval Neighborhood Logics.

[BibT_eX]

[DOI]

Proceedings of the Logical Foundations of Computer Science, International Symposium, 2007

2006

Relational dual tableaux for interval temporal logics.

[BibT_eX]

[DOI]

Joanna Golinska-Pilarek

Ewa Orlowska

J. Appl. Non Class. Logics, 2006

2005

A Tableau-Based Decision Procedure for Right Propositional Neighborhood Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2005

2004

Time Granularities and Ultimately Periodic Automata.

[BibT_eX]

[DOI]