Formula based abstractions of transition systems for real-time model checking

0Citations
Citations of this article
2Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

When verifying concurrent systems described by transition systems, state explosion is one of the most serious problems. If quantitative temporal information (expressed by clock ticks) are considered, state explosion is even more serious. In this paper we present a non-standard (abstract) semantics for the ASTP language able to produce reduced transition systems. The important point is that the abstract semantics produces transition systems equivalent to the standard ones for what concerns the satisfiability of a given set of formulae of a temporal logic with quantitative modal operators. The equivalence of transition systems with respect to formulae is expressed by means of ár,nñ-equivalence: two ár,nñ-equivalent transition systems give the same truth value to all formulae such that the actions occurring in the modal operators are contained in r, and with time constraints whose values are less than or equal to n.

Cite

CITATION STYLE

APA

Barbuti, R., De Francesco, N., Santone, A., & Vaglini, G. (1999). Formula based abstractions of transition systems for real-time model checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1708, pp. 289–306). Springer Verlag. https://doi.org/10.1007/3-540-48119-2_18

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free