\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb}
\usepackage{wasysym}
\usepackage[only,bigsqcap]{stmaryrd}

% this should be the last package used
\usepackage{pdfsetup}

\newcommand{\tv}{{\isacharprime}\,}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}


\begin{document}

\title{Formalization of Refinement Calculus for Reactive Systems}

\author{Viorel Preoteasa\\
Aalto University, Finland}

\maketitle

\begin{abstract}
We present a formalization of refinement calculus for reactive systems.
Refinement calculus is based on monotonic predicate transformers 
(monotonic functions from sets of post-states to sets of pre-states), 
and it is a powerful formalism for reasoning about imperative programs.
We model reactive systems as monotonic property transformers
that transform sets of output infinite sequences into sets of input
infinite sequences. Within this semantics we can model 
refinement of reactive systems, (unbounded) angelic and
demonic nondeterminism, sequential composition, and 
other semantic properties. We can model systems that may
fail for some inputs, and we can model compatibility of systems.
We can specify systems that have liveness properties using
linear temporal logic, and we can refine system specifications
into systems based on symbolic transitions systems, suitable
for implementations.

\end{abstract}

\tableofcontents

\parindent 0pt\parskip 0.5ex

\section{Introduction}

This is a formalization of refinement calculus for reactive 
systems that is presented in \cite{preoteasa:tripakis:2014tr}.

Refinement calculus \cite{back-1978,back-wright-98} has been
developed originally for input output imperative programs, and
is based on a predicate transformer semantics of programs with 
a weakest precondition interpretation.

We extend the standard refinement calculus to reactive systems
\cite{Harel:1989:DRS:101969.101990}. Within our framework a
reactive system is seen as a system that accepts as input
an infinite sequence of values and productes as output 
an infinite sequence of values. The semantics of these 
systems is given as {\em monotonic property transformers}.
These are monotonic functions which maps sets of output 
sequences (output properties) into sets of input sequences
(input properties). For a set of output sequences $q$, the
monotonic property transformer $S$ applied to $q$ returns
all input sequences from which the computation of $S$ 
always produces a sequence from $q$. 

Our work extends also the relational interfaces framework
of \cite{tripakis:2011} which can handle only finite safety 
properties to infinite properties and liveness.

This formalization is organized in three sections. 
Section 2 presents an algebraic formalization of 
linear temporal locic. Section 3 introduces basic
constructs from refinement calculus, and finally 
Section 4 applies the refinement calculus to reactive
systems. 



% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
