Compositional Termination Analysis of Symbolic Forward Analysis

Charatonik, Witold; Mukhopadhyay, Supratik; Podelski, Andreas; Cortesi, Agostino

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Compositional Termination Analysis of Symbolic Forward Analysis

MPS-Authors

/persons/resource/persons44232

Charatonik, Witold
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45084

Mukhopadhyay, Supratik
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45201

Podelski, Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Charatonik, W., Mukhopadhyay, S., & Podelski, A. (2002). Compositional Termination Analysis of Symbolic Forward Analysis. In Verification, Model Checking, and Abstract Interpretation. Third International Workshop, VMCAI 2002 (pp. 109-125). Berlin, Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-2F41-6

Abstract

Existing model checking tools for infinite state systems, such as UPPAAL, HYTECH and KRONOS, use symbolic forward analysis, a possibly nonterminating procedure. We give termination criteria that allow us to reason compositionally about systems defined with asynchronous parallel composition; we can prove the termination of symbolic forward analysis for a composed system from the syntactic conditions satisfied by the component systems. Our results apply to nonlinear hybrid systems; in particular to rectangular hybrid systems, timed automata and o-minimal systems. In the case of integer-valued systems we give negative results: forward analysis is not well-suited for this class of inite-state systems.