A Lattice Model to Verify Behavioral Equivalences

This paper presents a new model to verify behavioral equivalences based on behavior ontology. In the ontology, actions among processes or tasks are defined as interaction and movement, and, further, behaviors are defined as a sequence of such interactions and/or movements. Since some interactions and movements among the behaviors are overlapped, the behaviors are organized in a lattice structure, called, n:2-Lattice. Compared to other lattices, the lattice has special properties of multiple joins and meets. The property allows polymorphic interpretations of behaviors for equivalence, based on degree of abstraction. It guarantees abstraction of the exponential and nondeterministic complexity of behaviors into polynomial complexity. The ontology can be considered as one of the unique and innovative structure to represent behavioral equivalences.