Model-checking for hybrid systems by quotienting and constraints solving

Franck Cassez, François Laroussinie

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

21 Citations (Scopus)

Abstract

In this paper we present a semi-algorithm to do compositional model-checking for hybrid systems. We first define a modal logic Lhν which is expressively complete for linear hybrid automata. We then show that it is possible to extend the result on compositional model- checking for parallel compositions of finite automata and networks of timed automata to linear hybrid automata. Finally we present some results obtained with an extension of the tool CMC to handle a subclass of hybrid automata (the stopwatch automata).

Original languageEnglish
Title of host publicationComputer Aided Verification - 12th International Conference, CAV 2000, Proceedings
Place of PublicationBerlin; Heidelberg
PublisherSpringer, Springer Nature
Pages373-388
Number of pages16
Volume1855
ISBN (Print)3540677704
Publication statusPublished - 2000
Externally publishedYes
Event12th International Conference on Computer Aided Verification, CAV 2000 - Chicago, United States
Duration: 15 Jul 200019 Jul 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1855
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other12th International Conference on Computer Aided Verification, CAV 2000
CountryUnited States
CityChicago
Period15/07/0019/07/00

Fingerprint Dive into the research topics of 'Model-checking for hybrid systems by quotienting and constraints solving'. Together they form a unique fingerprint.

Cite this