关键词: 概率空间 Isabelle／HOL／Isar 定理证明

Abstract:

The paper describes concurrent systems with Paulson＇s inductive approach. In the paper, a set of generation sets is given, which is suitable for defining measures. The relation between the measure of finite executions and the measure of the sets of infinite runs is evaluated with a canonical function . It is proved that the measure of the sets of infinite runs is positive and eountably additive. With the Caratheodory＇s extension theorem, the probabi ility space on the set of infinite runs of concurrent systems is constructed. All scripts are checked with Isabell/HOL/Isar.

Key words: probability space, Isabelle/HOL/Isar, theorem proving