Commit e50e2851 authored by nipkow's avatar nipkow
Browse files

new article Timed-Automata

parent f370d197e854
......@@ -3420,6 +3420,34 @@ abstract = Recently, Javier Esparza and Jan Kretinsky proposed a new method dire
extra-history =
Change history: [2015-09-23]: Enable code export for the eager unfolding optimisation and reduce running time of the generated tool. Moreover, add support for the mlton SML compiler.
[Timed_Automata]
title = Timed Automata
author = Simon Wimmer <http://in.tum.de/~wimmers>
date = 2016-03-08
topic = Computer Science/Automata and Formal Languages
abstract =
Timed automata are a widely used formalism for modeling real-time
systems, which is employed in a class of successful model checkers
such as UPPAAL [LPY97], HyTech [HHWt97] or Kronos [Yov97]. This work
formalizes the theory for the subclass of diagonal-free timed
automata, which is sufficient to model many interesting problems. We
first define the basic concepts and semantics of diagonal-free timed
automata. Based on this, we prove two types of decidability results
for the language emptiness problem. The first is the classic result
of Alur and Dill [AD90, AD94], which uses a finite partitioning of
the state space into so-called `regions`. Our second result focuses
on an approach based on `Difference Bound Matrices (DBMs)`, which is
practically used by model checkers. We prove the correctness of the
basic forward analysis operations on DBMs. One of these operations is
the Floyd-Warshall algorithm for the all-pairs shortest paths problem.
To obtain a finite search space, a widening operation has to be used
for this kind of analysis. We use Patricia Bouyer's [Bou04] approach
to prove that this widening operation is correct in the sense that
DBM-based forward analysis in combination with the widening operation
also decides language emptiness. The interesting property of this
proof is that the first decidability result is reused to obtain the
second one.
[Parity_Game]
title = Positional Determinacy of Parity Games
author = Christoph Dittmann <http://logic.las.tu-berlin.de/Members/Dittmann/>
......
......@@ -241,6 +241,7 @@ SumSquares
TLA
Tail_Recursive_Functions
Tarskis_Geometry
Timed_Automata
Topology
TortoiseHare
Transitive-Closure
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
section \<open>Normalization of DBMs\<close>
theory DBM_Normalization
imports DBM_Basics
begin
text \<open>This is the implementation of the common approximation operation.\<close>
fun norm_upper :: "('t::time) DBMEntry \<Rightarrow> 't \<Rightarrow> ('t::time) DBMEntry"
where
"norm_upper e t = (if Le t \<prec> e then \<infinity> else e)"
fun norm_lower :: "('t::time) DBMEntry \<Rightarrow> 't \<Rightarrow> ('t::time) DBMEntry"
where
"norm_lower e t = (if e \<prec> Lt t then Lt t else e)"
text \<open>
Note that literature pretends that \<open>\<zero>\<close> would have some (presumably infinite bound) in \<open>k\<close>
and thus defines normalization uniformly. The easiest way to get around this seems to explicate
this in the definition as below.
\<close>
definition norm :: "('t::time) DBM \<Rightarrow> (nat \<Rightarrow> 't) \<Rightarrow> nat \<Rightarrow> 't DBM"
where
"norm M k n \<equiv> \<lambda> i j.
let ub = if i > 0 then (k i) else 0 in
let lb = if j > 0 then (- k j) else 0 in
if i \<le> n \<and> j \<le> n then norm_lower (norm_upper (M i j) ub) lb else M i j
"
section \<open>Normalization is a Widening Operator\<close>
lemma norm_mono:
assumes "\<forall>c. v c > 0" "u \<in> [M]\<^bsub>v,n\<^esub>"
shows "u \<in> [norm M k n]\<^bsub>v,n\<^esub>" (is "u \<in> [?M2]\<^bsub>v,n\<^esub>")
proof -
note A = assms
note M1 = A(2)[unfolded DBM_zone_repr_def DBM_val_bounded_def]
show ?thesis
proof (unfold DBM_zone_repr_def DBM_val_bounded_def, auto)
show "Le 0 \<preceq> ?M2 0 0"
using A unfolding norm_def DBM_zone_repr_def DBM_val_bounded_def dbm_le_def by auto
next
fix c assume "v c \<le> n"
with M1 have M1: "dbm_entry_val u None (Some c) (M 0 (v c))" by auto
from \<open>v c \<le> n\<close> A have *:
"?M2 0 (v c) = norm_lower (norm_upper (M 0 (v c)) 0) (- k (v c))"
unfolding norm_def by auto
show "dbm_entry_val u None (Some c) (?M2 0 (v c))"
proof (cases "M 0 (v c) \<prec> Lt (- k (v c))")
case True
show ?thesis
proof (cases "Le 0 \<prec> M 0 (v c)")
case True with * show ?thesis by auto
next
case False
with * True have "?M2 0 (v c) = Lt (- k (v c))" by auto
moreover from True dbm_entry_val_mono_2[OF M1] have
"dbm_entry_val u None (Some c) (Lt (- k (v c)))"
by auto
ultimately show ?thesis by auto
qed
next
case False
show ?thesis
proof (cases "Le 0 \<prec> M 0 (v c)")
case True with * show ?thesis by auto
next
case F: False
with M1 * False show ?thesis by auto
qed
qed
next
fix c assume "v c \<le> n"
with M1 have M1: "dbm_entry_val u (Some c) None (M (v c) 0)" by auto
from \<open>v c \<le> n\<close> A have *:
"?M2 (v c) 0 = norm_lower (norm_upper (M (v c) 0) (k (v c))) 0"
unfolding norm_def by auto
show "dbm_entry_val u (Some c) None (?M2 (v c) 0)"
proof (cases "Le (k (v c)) \<prec> M (v c) 0")
case True
with A(1,2) \<open>v c \<le> n\<close> have "?M2 (v c) 0 = \<infinity>" unfolding norm_def by auto
then show ?thesis by auto
next
case False
show ?thesis
proof (cases "M (v c) 0 \<prec> Lt 0")
case True with False * dbm_entry_val_mono_3[OF M1] show ?thesis by auto
next
case F: False
with M1 * False show ?thesis by auto
qed
qed
next
fix c1 c2 assume "v c1 \<le> n" "v c2 \<le> n"
with M1 have M1: "dbm_entry_val u (Some c1) (Some c2) (M (v c1) (v c2))" by auto
then show "dbm_entry_val u (Some c1) (Some c2) (?M2 (v c1) (v c2))"
proof (cases "Le (k (v c1)) \<prec> M (v c1) (v c2)")
case True
with A(1,2) \<open>v c1 \<le> n\<close> \<open>v c2 \<le> n\<close> have "?M2 (v c1) (v c2) = \<infinity>" unfolding norm_def by auto
then show ?thesis by auto
next
case False
with A(1,2) \<open>v c1 \<le> n\<close> \<open>v c2 \<le> n\<close> have
*: "?M2 (v c1) (v c2) = norm_lower (M (v c1) (v c2)) (- k (v c2))"
unfolding norm_def by auto
show ?thesis
proof (cases "M (v c1) (v c2) \<prec> Lt (- k (v c2))")
case True
with dbm_entry_val_mono_1[OF M1] have
"dbm_entry_val u (Some c1) (Some c2) (Lt (- k (v c2)))"
by auto
then have "u c1 - u c2 < - k (v c2)" by auto
with * True show ?thesis by auto
next
case False with M1 * show ?thesis by auto
qed
qed
qed
qed
end
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
session "Timed_Automata" = "HOL" +
options [timeout=600]
theories
Normalized_Zone_Semantics
document_files
"root.tex"
"root.bib"
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
# -*- shell-script -*-
# Get email when automated build fails. May be empty.
# values: "email1 email2 .. emailn"
NOTIFY="wimmers@in.tum.de"
# Participate in frequent (nightly) build (only for small submissions)
# values: "yes" "no"
FREQUENT="yes"
This diff is collapsed.
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}
% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed
\usepackage{amssymb}
%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
%\<triangleq>, \<yen>, \<lozenge>
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
% for uniform font size
\renewcommand{\isastyle}{\isastyleminor}
\renewcommand{\isamarkupchapter}[1]{\section{#1}}
\renewcommand{\isamarkupsection}[1]{\subsection{#1}}
\renewcommand{\isamarkupsubsection}[1]{\subsubsection{#1}}
\renewcommand{\isamarkupsubsubsection}[1]{\paragraph{#1}}
\begin{document}
\title{Timed Automata}
\author{Simon Wimmer}
\maketitle
\begin{abstract}
Timed automata are a widely used formalism for modeling real-time systems, which is employed
in a class of successful model checkers such as UPPAAL \cite{Larsen1997},
HyTech \cite{Henzinger97hytech} or Kronos \cite{Kronos97}.
This work formalizes the theory for the subclass of diagonal-free timed automata, which is
sufficient to model many interesting problems.
We first define the basic concepts and semantics of diagonal-free timed automata.
Based on this, we prove two types of decidability results for the language emptiness problem.
The first is the classic result of Alur and Dill \cite{alur_automata_1990,alur_theory_1994},
which uses a finite partitioning of the state space into so-called \textit{regions}.
Our second result focuses on an approach based on \textit{Difference Bound Matrices (DBMs)},
which is practically used by model checkers.
We prove the correctness of the basic forward analysis operations on DBMs.
One of these operations is the Floyd-Warshall algorithm for the all-pairs
shortest paths problem.
To obtain a finite
search space, a widening operation has to be used for this kind of analysis.
We use Patricia Bouyer's \cite{Bou_Forward_Analysis} approach to prove that this widening operation
is correct in the sense that DBM-based forward analysis in combination with the widening operation
also decides language emptiness. The interesting property of this proof is that the first
decidability result is reused to obtain the second one.
\end{abstract}
\setcounter{tocdepth}{2}
\tableofcontents
\newpage
% sane default for proof documents
\parindent 0pt\parskip 0.5ex
% generated text of all theories
\input{session}
% optional bibliography
\bibliographystyle{alpha}
\bibliography{root}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment