An Equivalent CTL Formulation for Condition Sequences
| Autor: | Lawrence E. Holloway, J. Ashley |
|---|---|
| Rok vydání: | 2005 |
| Předmět: |
Structure (mathematical logic)
Sequential logic Computation tree logic Computer science Programming language Petri net computer.software_genre Linear temporal logic Control and Systems Engineering Modeling and Simulation Probabilistic CTL Temporal logic State (computer science) Electrical and Electronic Engineering computer |
| Zdroj: | Discrete Event Dynamic Systems. 15:333-348 |
| ISSN: | 1573-7594 0924-6703 |
| DOI: | 10.1007/s10626-005-4056-0 |
| Popis: | A condition system is a form of Petri net that interacts with other condition systems and the environment via state-based signals called conditions. The condition language framework has been used in previous papers to characterize the input/output behavior of such interacting systems, as well as to specify desired control behavior among other things. In this paper, we show that condition sequences (the specification) and condition systems (the model of the system) have an equivalent structure in the computation tree logic (CTL) framework. The primary goals of this work are to be able to utilize existing tools for program verification for our systems, and to make our work more accessible to the temporal logic community. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink