Search engine for discovering works of Art, research articles, and books related to Art and Culture
Javascript must be enabled to continue!
Bounded Model Checking of Continuous Stochastic Logic
View through CrossRef
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 explosion is the main obstacle
making the technique more practical. To avoid the state explosion, a
bounded model checking technique of continuous stochastic logic is
proposed. First of all, the bounded semantics of continuous stochastic
logic is presented, and its correctness is proven. Secondly, an
effective method for computing the transient probability and
steady-state probability bounded by the path length is proposed.
Finally, for different operators bounded model checking procedures based
on the computation of the transient probability and steady-state
probability bounded by the path length are proposed. The experiment
results show that if the property can be verified in local reachable
space with small depth, then the bounded model checking is better than
global model checking in time and space consumption.
Title: Bounded Model Checking of Continuous Stochastic Logic
Description:
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 explosion is the main obstacle
making the technique more practical.
To avoid the state explosion, a
bounded model checking technique of continuous stochastic logic is
proposed.
First of all, the bounded semantics of continuous stochastic
logic is presented, and its correctness is proven.
Secondly, an
effective method for computing the transient probability and
steady-state probability bounded by the path length is proposed.
Finally, for different operators bounded model checking procedures based
on the computation of the transient probability and steady-state
probability bounded by the path length are proposed.
The experiment
results show that if the property can be verified in local reachable
space with small depth, then the bounded model checking is better than
global model checking in time and space consumption.
Related Results
Model-checking ecological state-transition graphs
Model-checking ecological state-transition graphs
Abstract
Model-checking is a methodology developed in computer science to automatically assess the dynamics of discrete systems, by checking if a system modelled as...
MECHANISMS OF SCHEMATIC MODELING BASED ON VECTOR LOGIC
MECHANISMS OF SCHEMATIC MODELING BASED ON VECTOR LOGIC
Context. This paper addresses issues relevant to the EDA market – reducing the cost and time of testing and verification of digital projects by synthesizing the logic vector of a d...
Logic in the early 20th century
Logic in the early 20th century
The creation of modern logic is one of the most stunning achievements of mathematics and philosophy in the twentieth century. Modern logic – sometimes called logistic, symbolic log...
Bounded Correctness Checking of the Universal Fragment of eCTL
Bounded Correctness Checking of the Universal Fragment of eCTL
Bounded model checking as a complementary approach to BDD based symbolic model checking applies satisfiability checking to the verification of temporal properties, especially, for ...
Memristor-Based Priority Encoder and Decoder Circuit
Memristor-Based Priority Encoder and Decoder Circuit
Introduction:
Memristors, recognized as the fourth fundamental circuit element, exhibit unique features
such as non-volatility, scalability, and energy efficien...
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...
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...
On a non-standard two-species stochastic competing system and a related degenerate parabolic equation
On a non-standard two-species stochastic competing system and a related degenerate parabolic equation
We propose and analyse a new stochastic competing two-species population dynamics model. Competing algae population dynamics in river environments, an important engineering problem...