Email Gateway (Aug 22 2022 at 17:21): Email Gateway (Aug 22 2022 at 17:21):From: Lawrence Paulson <lp15@cam.ac.uk>
It never rains but it pours. Today we have two new entries, which are concerned with probability:
Probabilistic Timed Automata
We present a formalization of probabilistic timed automata (PTA) for which we try to follow the formula MDP + TA = PTA as far as possible: our work starts from our existing formalizations of Markov decision processes (MDP) and timed automata (TA) and combines them modularly. We prove the fundamental result for probabilistic timed automata: the region construction that is known from timed automata carries over to the probabilistic setting. In particular, this allows us to prove that minimum and maximum reachability probabilities can be computed via a reduction to MDP model checking, including the case where one wants to disregard unrealizable behavior.
https://www.isa-afp.org/entries/Probabilistic_Timed_Automata.html
Hidden Markov Models
This entry contains a formalization of hidden Markov models [3] based on Johannes Hölzl's formalization of discrete time Markov chains [1]. The basic definitions are provided and the correctness of two main (dynamic programming) algorithms for hidden Markov models is proved: the forward algorithm for computing the likelihood of an observed sequence, and the Viterbi algorithm for decoding the most probable hidden state sequence. The Viterbi algorithm is made executable including memoization. Hidden markov models have various applications in natural language processing.
https://www.isa-afp.org/entries/Hidden_Markov_Models.html
Many thanks to Simon Wimmer and Johannes Hölzl!
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC