Publications
You can find below the complete list of my publications.
Conferences
- C. Jegourel, A. Legay, S. Sedwards An Effective Heuristic for Adaptive Importance Splitting in Statistical Model Checking
Accepted to ISoLA'14, october 2014.
Abstract | Pdf
Keywords: statistical model checking, importance splitting, score function, importance sampling, rare events, temporal logic, reliability, biochemistry
Abstract: Statistical model checking avoids the intractable growth of states associated with numerical model checking by estimating the probability of a property from simulations. Rare properties pose a challenge because the relative error of the estimate is unbounded. In CAV'13, we describe how importance splitting may be used with SMC to overcome this problem. The basic idea is to decompose a logical property into nested properties whose probabilities are easier to estimate. To improve performance it is desirable to decompose the property into many equi-probable levels, but logical decomposition alone may be too coarse. In this article we make use of the notion of a score function to improve the granularity of a logical property. We show that such a score function may take advantage of heuristics, so long as it also rigorously respects certain properties. To demonstrate our importance splitting approach we present an optimal adaptive importance splitting algorithm and an heuristic score function. We give experimental results that demonstrate a significant improvement in performance over alternative approaches. - U. Fahrenberg, F. Biondi,
K. Corre, C. Jegourel,
S. Kongshoj, A. Legay Measuring Global Similarity between Texts
Accepted to SLSP'14, september 2014.
Abstract | Pdf
Keywords: statistical model checking, importance splitting, score function, importance sampling, rare events, temporal logic, reliability, biochemistry
Abstract: We propose a new similarity measure between texts which, contrary to the current state-of-the-art approaches, takes a global view of the texts to be compared. We have implemented a tool to compute our textual distance and conducted experiments on several corpuses of texts. The experiments show that our methods can reliably identify different global types of texts. - C. Jegourel, A. Legay, S. Sedwards Importance Splitting for Statistical Model Checking Rare Properties
Accepted to CAV'13, july 2013.
Abstract | Pdf
Keywords: statistical model checking, importance splitting, score function, importance sampling, rare events, temporal logic, reliability, biochemistry
Abstract: Statistical model checking avoids the intractable growth of states associated with probabilistic model checking by estimating the probability of a property from simulations. Rare properties are often important, but pose a challenge for simulation-based approaches: the relative error of the estimate is unbounded. A key objective for statistical model checking rare events is thus to reduce the variance of the estimator. Importance splitting achieves this by estimating a sequence of conditional probabilities, whose product is the required result. To apply this idea to model checking it is necessary to define a score function based on logical properties, and a set of levels that delimit the conditional probabilities. In this paper we motivate the use of importance splitting for statistical model checking and describe the necessary and desirable properties of score functions and levels. We illustrate how a score function may be derived from a property and give two importance splitting algorithms: one that uses fixed levels and one that discovers optimal levels adaptively. - S. Bensalem, M. Bozga, B. Delahaye, C. Jegourel, A. Legay, A. Nouri Statistical Model Checking QoS properties of Systems with SBIP
Accepted to ISOLA'12, october 2012.
Abstract | Pdf
Keywords: statistical model checking, large systems, BIP, monitors
Abstract: BIP is a component-based framework supporting rigorous design of embedded systems. This paper presents SBIP, an extension of BIP that relies on a new stochastic semantics that enables verification of large-size systems by using Statistical Model Checking. The approach is illustrated on several industrial case studies. - C. Jegourel, A. Legay, S. Sedwards Cross entropy optimisation of importance sampling parameters for statistical model checking
Accepted to CAV'12, july 2012.
Abstract | Pdf
Keywords: statistical model checking, importance sampling, rare events, cross-entropy, parametrised tilting, reliability, biochemistry
Abstract: Statistical model checking avoids the exponential growth of states associated with probabilistic model checking by estimating properties from multiple executions of a system and by giving results within confidence bounds. Rare properties are often very important but pose a particular challenge for simulation-based approaches, hence a key objective under these circumstances is to reduce the number and length of simulations necessary to produce a given level of confidence. Importance sampling is a well-established technique that achieves this, however to maintain the advantages of statistical model checking it is necessary to find good importance sampling distributions without considering the entire state space. Motivated by the above, we present a simple algorithm that uses the notion of cross-entropy to find the optimal parameters for an importance sampling distribution. In contrast to previous work, our algorithm uses a low dimensional vector of parameters to define this distribution and thus avoids the often intractable explicit representation of a transition matrix. We show that our parametrisation leads to a unique optimum and can produce many orders of magnitude improvement in simulation efficiency. We demonstrate the efficacy of our methodology by applying it to models from reliability engineering and biochemistry. - C. Jegourel, A. Legay, S. Sedwards A Platform for High Performance Statistical Model Checking - PLASMA
Accepted to TACAS'12, february 2012.
Abstract | Pdf
Keywords: statistical model checking, importance sampling, rare events, reliability modelling, systems biology.
Abstract: Statistical model checking offers the potential to decide and quantify dynamical properties of models with intractably large state space, opening up the possibility to verify the performance of complex real-world systems. Rare properties and long simulations pose a challenge to this approach, so here we present a fast and compact statistical model checking platform, PLASMA, that incorporates an efficient simulation engine and features an importance sampling engine to reduce the number and length of simulations when properties are rare. For increased flexibility and efficiency PLASMA compiles both model and property into bytecode that is executed on an in-built memory-efficient virtual machine.
Journals
- S. Bensalem, M. Bozga, B. Delahaye, C. Jegourel, A. Legay, A. Nouri Statistical Model Checking QoS properties of Systems with SBIP
International Journal on Software Tools for Technology Transfer, 1-15, to appear, 2014.
Abstract | Pdf
Keywords: statistical model checking, large systems, BIP, monitors
BIP is a component-based framework supporting rigorous design of embedded systems. BIP supports incremental design of large systems from atomic components that communicates via connectors and whose interactions can be described with a powerful algebra. This paper presents SBIP, an extension of BIP for stochastic systems. SBIP offers the possibility to add stochastic information to atomic component's behaviors, and hence to the entire system. Atomic component's semantics in SBIP is described by Markov Chains. We show that the semantics of the entire system is described by a Markov chain, showing that the non-determinism arising from system interactions is automatically eliminated by BIP. This allows us to verify systems described in SBIP with Statistical Model Checking. This paper introduces SBIP and illustrates its usability on several industrial case studies.
Other publications
- F. Cérou, T. Furon, A. Guyader, C. Jegourel Estimating the Probability of False Alarm.
DSP'09, july 2009.
Abstract | Pdf
Keywords: Watermarking, False alarm, Rare event analysis.
Abstract: Assessing that a probability of false alarm is below a given significance level is a crucial issue in watermarking. We propose an iterative and self-adapting algorithm which estimates very low probabilities of error. Some experimental investigations validates its performance for a rare detection scenario where there exists a close form formula of the probability of false alarm. Our algorithm appears to be much quicker and more accurate than a classical Monte Carlo estimator. It even allows the experimental measurement of error exponents.