Process modeling with different qualities of knowledge
- 104 Downloads
For modeling structured processes with different levels of atomic actions, classical linear or branching time Kripke structures with first-order states are insufficient: They do not provide any means for modeling independent parallel threads of activity which have to be joined at some point, action refinement, or procedure concepts. In all three cases, it is important to distinguish facts resp. knowledge derived in the current thread of activity from facts which are not concerned in this activity. This problem is also closely related to the frame problem.
In this paper, hierarchical Kripke structures are introduced for modeling hierarchically structured processes, also coping with the different qualities of knowledge arising in this context: every state consists of a total first-order interpretation, which gives the state as-is, and a partial first-order interpretation containing all procedure knowledge which has been derived in the current thread of activity.
A correct and complete set of axioms is presented for reasoning about hierarchical Kripke structures.
KeywordsProcedure Knowledge Accessibility Relation Parallel Composition Predicate Symbol Auxiliary State
Unable to display preview. Download preview PDF.
- [AH93]L. Aceto and M. Hennessy. Towards Action-Refinement in Process Algebras. Information and Computation, 103, 1993.Google Scholar
- [AH96]R. Alur and T. Henzinger. Reactive Modules. In Proc. 11th Symp. on Logic in Computer Science (LICS), 1996.Google Scholar
- [BHK90]J. Bergstra, J. Heering, and P. Klint. Module Algebra. Journal of the ACM, 37(2):335–372, 1990.Google Scholar
- [BK94]A. J. Bonner and M. Kifer. An Overview of Transaction Logic. Theoretical Computer Science, 133(2):205–265, 1994.Google Scholar
- [DG91]P. Degano and R. Gorrieri. Atomic refinement in Process Description languages. In 16th Symp. on Mathematical Foundations of Computer Science, Springer LNCS 520, pp. 121–130, 1991.Google Scholar
- [DG95]P. Degano and R. Gorrieri. A Causal Operational Semantics of Action Refinement. Information and Computation, 122(1):97–119, 1995.Google Scholar
- [Har79]D. Harel. First-Order Dynamic Logic, Springer LNCS 68, 1979.Google Scholar
- [HM85]M. Hennessy and R. Milner. Algebraic Laws for Non-determinism and Concurrency. Journal of the ACM, 32:137–161, 1985.Google Scholar
- [LML96]B. Ludäscher, W. May, and G. Lausen. Nested Transactions in a Logical Language for Active Rules. In Proc. Intl. Workshop on Logic in Databases (LID), San Miniato, Italy, Springer LNCS 1154, pp. 197–222, 1996.Google Scholar
- [May97]W. May. Specifying Complex and Structured Systems with Evolving Algebras. In Proc. TAPSOFT'97, To appear in Springer LNCS Series, 1997.Google Scholar
- [MH69]J. McCarthy and P. Hayes. Some Philosophical Problems from the Stand-point of Artificial Intelligence. In B. Meltzer and D. Michie, editors, Machine Intelligence 4, pages 463–502. Edinburgh University Press, 1969.Google Scholar