Search engine for discovering works of Art, research articles, and books related to Art and Culture
Javascript must be enabled to continue!
Bounded Correctness Checking of the Universal Fragment of eCTL
View through CrossRef
Bounded model checking as a complementary approach to BDD based symbolic model checking applies satisfiability checking to the verification of temporal properties, especially, for efficient error detection. The successes of bounded model checking have led to extensive research on bounded semantics for various (fragments of) temporal logics such as ACTL, ECTL, and ACTL*. We in this paper further study AeCTL formulas (universal fragment of extended Computation Tree Logic) in light of bounded semantics. On the theoretical aspect, we propose a bounded correctness checking algorithm for AeCTL properties. On the practical aspect, we apply the bounded semantics of AeCTL to derive a SAT-based characterization of AeCTL properties.
Title: Bounded Correctness Checking of the Universal Fragment of eCTL
Description:
Bounded model checking as a complementary approach to BDD based symbolic model checking applies satisfiability checking to the verification of temporal properties, especially, for efficient error detection.
The successes of bounded model checking have led to extensive research on bounded semantics for various (fragments of) temporal logics such as ACTL, ECTL, and ACTL*.
We in this paper further study AeCTL formulas (universal fragment of extended Computation Tree Logic) in light of bounded semantics.
On the theoretical aspect, we propose a bounded correctness checking algorithm for AeCTL properties.
On the practical aspect, we apply the bounded semantics of AeCTL to derive a SAT-based characterization of AeCTL properties.
Related Results
Model-checking ecological state-transition graphs
Model-checking ecological state-transition graphs
AbstractModel-checking is a methodology developed in computer science to automatically assess the dynamics of discrete systems, by checking if a system modelled as a state-transiti...
Bounded Model Checking of Continuous Stochastic Logic
Bounded Model Checking of Continuous Stochastic Logic
Model checking continuous stochastic logic has been proven to be a
powerful technique for analyzing the dependability and performance of
stochastic systems. The state space explosi...
Evolution of a course on model checking for practical applications
Evolution of a course on model checking for practical applications
Although model checking is expected as a practical formal verification approach for its automatic nature, it still suffers from difficulties in writing the formal descriptions to b...
Clock monitoring is associated with age-related decline in time-based prospective memory
Clock monitoring is associated with age-related decline in time-based prospective memory
AbstractIn laboratory time-based prospective memory tasks, older adults typically perform worse than younger adults do. It has been suggested that less frequent clock checking due ...
Hodge–Dirac, Hodge-Laplacian and Hodge–Stokes operators in $L^p$ spaces on Lipschitz domains
Hodge–Dirac, Hodge-Laplacian and Hodge–Stokes operators in $L^p$ spaces on Lipschitz domains
This paper concerns Hodge–Dirac operators
D_{{}^\Vert}=d+\underline{\delta}
acting in
L^p(\Omega, ...
On bounded generalized Harish-Chandra modules
On bounded generalized Harish-Chandra modules
Let ???? be a complex reductive Lie algebra and ????⊂???? be any reductive in ???? subalgebra. We call a (????,????)-module M bounded if the ????-multiplicities of M are uniformly ...
Numerical simulation of fragment impacting solid rocket motors
Numerical simulation of fragment impacting solid rocket motors
For the initiation characteristics of solid rocket motors (SRMs) filled with high-energy solid propellant under fragment impact, the related theoretical critical criterion for shoc...
Probabilistic Model Checking for Biology
Probabilistic Model Checking for Biology
Probabilistic model checking is an automated method for verifying the correctness and performance of probabilistic models. Property specifications are expressed in probabilistic te...