-
Decisiveness of Stochastic Systems and its Application to Hybrid Models (Full Version)
Authors:
Patricia Bouyer,
Thomas Brihaye,
Mickael Randour,
Cédric Rivière,
Pierre Vandenhove
Abstract:
In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisive…
▽ More
In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems.
[ABM07] Parosh A. Abdulla, Noomene Ben Henda, and Richard Mayr. 2007. Decisive Markov Chains. Log. Methods Comput. Sci. 3, 4 (2007).
△ Less
Submitted 10 January, 2022; v1 submitted 28 September, 2020;
originally announced September 2020.
-
Decisiveness of Stochastic Systems and its Application to Hybrid Models
Authors:
Patricia Bouyer,
Thomas Brihaye,
Mickael Randour,
Cédric Rivière,
Pierre Vandenhove
Abstract:
In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisive…
▽ More
In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems. [ABM07] Parosh A. Abdulla, Noomene Ben Henda, and Richard Mayr. 2007. Decisive Markov Chains. Log. Methods Comput. Sci. 3, 4 (2007).
△ Less
Submitted 22 September, 2020; v1 submitted 13 January, 2020;
originally announced January 2020.
-
A genetic algorithm applied to the validation of building thermal models
Authors:
Alfred Jean Philippe Lauret,
Harry Boyer,
Carine Riviere,
Alain Bastide
Abstract:
This paper presents the coupling of a building thermal simulation code with genetic algorithms (GAs). GAs are randomized search algorithms that are based on the mechanisms of natural selection and genetics. We show that this coupling allows the location of defective sub-models of a building thermal model i.e. parts of model that are responsible for the disagreements between measurements and model…
▽ More
This paper presents the coupling of a building thermal simulation code with genetic algorithms (GAs). GAs are randomized search algorithms that are based on the mechanisms of natural selection and genetics. We show that this coupling allows the location of defective sub-models of a building thermal model i.e. parts of model that are responsible for the disagreements between measurements and model predictions. The method first of all is checked and validated on the basis of a numerical model of a building taken as reference. It is then applied to a real building case. The results show that the method could constitute an efficient tool when checking the model validity.
△ Less
Submitted 18 December, 2012;
originally announced December 2012.
