Probabilities in Action Systems. Sekerinski, E., Sere, K., & Troubitsyna, E. December, 1996.
Probabilities in Action Systems [link]Paper  abstract   bibtex   
Action systems combined with the refinement calculus \citeBaKu83,BaSe94:FME is a powerful tool for the design of parallel and distributed systems in a stepwise manner. The basic idea behind action systems is that actions are atomic entities that are chosen for execution nondeterministically. In many situations, especially when designing of control systems \citeBuSS96, some preliminary information regarding probabilities of execution of certain actions is given. Within action systems we cannot take this information into account and hence we get only a pessimistic estimation of system behavior. The formalism is based on the predicate transformer semantics. Recently the notion of probabilistic predicate transformers has been introduced \citeMorg96 to reason about probabilistic behavior of programs as well as refinement. We propose a way of combining the probabilistic predicate transformer theory with the action systems formalism and identify a class of action systems where such merging is possible. We \em embed a probabilistic actions, i.e. actions where a choice of action is performed probabilistically, into a nondeterministic action system. Thus in a probabilistic action system some of the nondeterministic choices are replaced by probabilistic choices. We show that the introduction of probabilistic action systems still allows us to perform refinement of action systems in an ordinary way. Thus we can reason about the correctness of probabilistic tasks within the refinement calculus for action systems. \bibitemBaKu83 R. J. R. Back and R. Kurki-Suonio. \newblock Decentralization of process nets with centralized control. \newblock In \em Proc.\ of the 2nd ACM SIGACT–SIGOPS Symp. on Principles of Distributed Computing, pages 131–142, 1983. \bibitemBaSe94:FME R. J. R. Back and K. Sere. \newblock From modular systems to action systems. \newblock Proc.\ of \em Formal Methods Europe'94, Spain, October 1994. \newblock \em Lecture Notes in Computer Science. Springer–Verlag, 1994. \bibitemBuSS96 M. Butler, E. Sekerinski, and K. Sere. An Action System Approach to the Steam Boiler Problem. In Jean-Raymond Abrial, Egon Borger and Hans Langmaack, editors, \em Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, Lecture Notes in Computer Science Vol. 1165. Springer-Verlag, 1996. To appear. \bibitemMorg96 K. Seidel, C.C. Morgan and A.K. McIver. \newblock An introduction to probabilistic predicate transformers. \newblock \em Technical report PRG-TR-6-96, Programming Research Group, 1996.
@misc{SekerinskiSereTroubitsyna96ProbabilitiesActionSystems,
	address = {Oslo, Norway},
	title = {Probabilities in {Action} {Systems}},
	url = {https://web.archive.org/web/19970606115810/http://www.ifi.uio.no/~nwpt96/},
	abstract = {Action systems combined with the refinement calculus {\textbackslash}citeBaKu83,BaSe94:FME is a powerful tool for the design of parallel and distributed systems in a stepwise manner. The basic idea behind action systems is that actions are atomic entities that are chosen for execution nondeterministically. In many situations, especially when designing of control systems {\textbackslash}citeBuSS96, some preliminary information regarding probabilities of execution of certain actions is given. Within action systems we cannot take this information into account and hence we get only a pessimistic estimation of system behavior. The formalism is based on the predicate transformer semantics. Recently the notion of probabilistic predicate transformers has been introduced {\textbackslash}citeMorg96 to reason about probabilistic behavior of programs as well as refinement. We propose a way of combining the probabilistic predicate transformer theory with the action systems formalism and identify a class of action systems where such merging is possible. We {\textbackslash}em embed a probabilistic actions, i.e. actions where a choice of action is performed probabilistically, into a nondeterministic action system. Thus in a probabilistic action system some of the nondeterministic choices are replaced by probabilistic choices. We show that the introduction of probabilistic action systems still allows us to perform refinement of action systems in an ordinary way. Thus we can reason about the correctness of probabilistic tasks within the refinement calculus for action systems. {\textbackslash}bibitemBaKu83 R. J. R. Back and R. Kurki-Suonio. {\textbackslash}newblock Decentralization of process nets with centralized control. {\textbackslash}newblock In {\textbackslash}em Proc.{\textbackslash} of the 2nd ACM SIGACT–SIGOPS Symp. on Principles of Distributed Computing, pages 131–142, 1983. {\textbackslash}bibitemBaSe94:FME R. J. R. Back and K. Sere. {\textbackslash}newblock From modular systems to action systems. {\textbackslash}newblock Proc.{\textbackslash} of {\textbackslash}em Formal Methods Europe'94, Spain, October 1994. {\textbackslash}newblock {\textbackslash}em Lecture Notes in Computer Science. Springer–Verlag, 1994. {\textbackslash}bibitemBuSS96 M. Butler, E. Sekerinski, and K. Sere. An Action System Approach to the Steam Boiler Problem. In Jean-Raymond Abrial, Egon Borger and Hans Langmaack, editors, {\textbackslash}em Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, Lecture Notes in Computer Science Vol. 1165. Springer-Verlag, 1996. To appear. {\textbackslash}bibitemMorg96 K. Seidel, C.C. Morgan and A.K. McIver. {\textbackslash}newblock An introduction to probabilistic predicate transformers. {\textbackslash}newblock {\textbackslash}em Technical report PRG-TR-6-96, Programming Research Group, 1996.},
	author = {Sekerinski, Emil and Sere, Kaisa and Troubitsyna, Elena},
	month = dec,
	year = {1996},
}

Downloads: 0