Efficient model checking for duration calculus based on branching-time approximations

Martin Fränzle, Michael Reichhardt Hansen

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    Abstract

    Duration Calculus (abbreviated to DC) is an interval-based, metric-time temporal logic designed for reasoning about embedded real-time systems at a high level of abstraction. But the complexity of model checking any decidable fragment featuring both negation and chop, DC's only modality, is non-elementary and thus impractical. We here investigate a similar approximation as frequently employed in model checking situation-based temporal logics, where linear-time problems are safely approximated by branching-time counterparts amenable to more efficient model-checking algorithms. Mimicking the role that a situation has in (A)CTL as origin of a set of linear traces, we define a branching-time counterpart to interval-based temporal logics building on situation pairs spanning sets of intervals. While this branching-time interval semantics yields the desired reduction in complexity of the model-checking problem, from non-elementary to linear in the size of the formula and cubic in the size of the model, the approximation is too coarse to be practical. We therefore refine the semantics by an occurrence count for crucial states (e.g., cuts of loops) in the model, arriving at a 4-fold exponential model-checking problem sufficiently accurately approximating the original one.
    Original languageEnglish
    Title of host publicationSixth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2008)
    Place of PublicationCape Town
    PublisherIEEE
    Publication date2008
    Pages63-72
    ISBN (Print)07-69-53437-6
    DOIs
    Publication statusPublished - 2008
    EventSixth IEEE International Conference on Software Engineering and Formal Methods - Cape Town
    Duration: 1 Jan 2008 → …

    Conference

    ConferenceSixth IEEE International Conference on Software Engineering and Formal Methods
    CityCape Town
    Period01/01/2008 → …

    Fingerprint

    Dive into the research topics of 'Efficient model checking for duration calculus based on branching-time approximations'. Together they form a unique fingerprint.

    Cite this