A first order temporal logic for behavior representation

Abstract

An important problem for knowledge representation is the specification of the behavior of information systems. To solve this problem, different formal techniques have been used and many authors have endorsed the use of different sorts of logics. This problem is even more important in software engineering, where the main modeling languages are defined with no formal semantics. For example UML 2.0 has been proposed using a textual semantics. This work has a twofold objective: Firstly, we introduce a novel modal temporal logic called LNi1, which is the natural extension to first order of LNint-e, presented in [17, 7]. Secondly, we show the usefulness of our logic for solving an important and specific knowledge representation problem: Providing UML with a formal semantics (focusing on state machines). This way we want both to avoid the disadvantages of current textual UML semantics and to provide a formal basis for further verification and validation of UML models. Our new logic LNi 1 overcomes the two main limitations of LNint-e in the formalization of UML state machines: the use of parameters in the operations and the specification of the communications between objects. © Springer-Verlag Berlin Heidelberg 2004.