AP03_5.vp 1 Introduction The main problem of CAD systems is how to represent designed objects, how to represent design knowledge and primarily how to represent the design process itself. The problem of representation of the design process and its components has been solved since CAD systems came into existence. The question of how to represent the design pro- cess still remains open. There is no common universal theoretical model for describing the design process nor are there any standards for design process representation. This situation is similar that 20 – 30 years ago in computer graph- ics. There were a great number of geometrical modelers that served as the kernels of CAD systems. The consequence of this situation is obvious even today – CAD systems have poor compatibility. The principles of design theory were formulated among others in [2]. A general design theory based on the principle of metamodel first appeared in [3], then later, e.g., in [4] and [5]. The idea of design theory again evokes a new discussion activity. A fresh critical view on the extended general theory and the theory of the metamodel appeared in [6]. In [7] there is a discussion of a new idea for using a formal means of modal logic for design process description. Lately, a number of papers have appeared which are searching for new meth- ods to describe the design process – for example: by means of analysis of a design protocol [8], by means of a relational system [9], with the help of a set-theory model [10], an object-oriented approach [11], etc. There is a growing effort to overcome the gap in describing the design process. In this paper we try to formalize the design process by means of one type of non-standard logic – modal logic [1]. The reason for this choice is the ability of this formalism to describe modeling of the individual discrete steps of design, design process branching, respecting necessity or possibility types of de- sign knowledge. 2 Modal logic One way to define modal logic is by extending of the clas- sical axiomatic definition of propositional logic by adding some other connectives (modal connectives), and the de- ductive system of propositional logic can be extended with axioms and inference rules characterizing modal logic. First, two alethic modalities – modality of necessity and modality of possi- bility – will be introduced and represented by symbols � and �. The expression ,p will be read as “it is necessary that p” and ex- pression � p as “it is possible that p”. The language of proposi- tional modal logic will be enriched by these two symbols, i.e., modal logic language will contain the following connectives: �, �, �, �, �, � and �. Modal logic language syntax is deter- mined by two rules: 1. All propositional logic formulas are also modal proposi- tional logic formulas. 2. If p is a modal propositional logic formula then formulas � p and �p are also formulas of this logic. Connectives of necessity and possibility are connected according to the following definition: � � �p def � � p which can be informally interpreted as, e.g. “if something is possible, then it is not true that it is necessary for it to be in- valid”. Some other interpretations are given, e.g., in [1, 14]. Several axiomatic systems exist which characterize the respective modal propositional logic system [1]. Here, some of the systems will be shown and one the most appropriate for our purpose will be chosen. Attention will be focused on the term accessibility relation, which is closely connected to the modal logic structure of axioms, after which some axiomatic systems will be shown [1]. Unlike classical propositional logic, modal logic formulas cannot be simply interpreted in an extensional way. Modal connectives are operators of an intens- ional character – which means that interpretation of a formula that contains modal operators is not possible if based only on knowledge of the individual subformula values and applica- tion of logical operations represented by the semantics of these connectives. The interpretation is extended by different world images in which the logic formulas can be evaluated in a different way. A world is an element of a semantic environment for the interpretation of modal logic formulas. This environment has a finite non-zero number of elements, or worlds. Modal logic did not need this image because it is, from the formula inter- pretation point of view, an enclosed system. Interpretation of a formula depends only on the individual subformulas “in one given world of interpretation – given state of things”. For the final image, it is possible to imagine a world as one possible state of a tested reality description, the state of the investigated reality. © Czech Technical University Publishing House http://ctn.cvut.cz/ap/ 3 Acta Polytechnica Vol. 43 No. 5/2003 Modal Logic – a Tool for Design Process Formalisation I. Jelínek In this paper we show the possibility to formalize the design process by means of one type of non-standard logic – modal logic [1]. The type chosen for this study is modal logic S4. The reason for this choice is the ability of this formalism to describe modeling of the individual discrete steps of design, respecting necessity or possibility types of design knowledge. Keywords: modal logic, accessibility relation, design process, formalisation of design process. Interpretation of modal logic formulas can depend not only on subformula values in the given world but also on for- mula values in worlds which have some connection with the considered actual world of evaluation. And it is on the very properties of the given world connection with other worlds that the character of different modal logic systems is built. The given world connection to other connected worlds is characterized by the accessibility relation [1, 14]. Modal logic formula interpretation is thus conducted within the frame of the accessible worlds. Let us introduce the frame of worlds [1] (structure [14]) formally as an ordered couple: � �F W R� , , where W set of worlds, R R W W� � , binary relation (accessibility relation). Now let us introduce the term model (compare to the term model for propositional logic, where it was determined only by evaluation). Let P be a set of atomic formulas. Let us sym- bolize as L (P) the set of formulas which can be generated from P. The model (P-model) within the frame � �F W R� , will be then called a triad: � �M W R V� , , where V: P � 2W. V maps each atomic formula p P� to the subset � �V p W� and therefore represents all worlds w W� in which p is valid. The validity of formula A in a given world W and model M will be symbolized as follows: M �w A and will be defined recursively: M � �w F (false) M �w p if � �w V p p P� �, M �w X � Y if M �w X implies M �w Y M �w � A if wRt implies M �w A for all worlds t � W and possibly we can add definitions of other connectives: M �w X � Y if M �w X and simultaneously M �w Y M �w X � Y if M �w X or M �w Y M �w �X if M � �w X M �w � A if wRt implies M �w A for at least one world t � W. Formula � �A L P� is valid in a model � �M W R V� , , , if A is valid in all worlds of the model M, i.e. M �w A for all w W� . Symbolized as: M � A. Formula � �A L P� is valid within the frame � �F W R� , , if A is valid in every model � �M W R V� , , , i.e. M � A it means for every model � �M W R V� , , . Symbolized as: F � A. Formula � �A L P� is valid if A is valid in every frame, i.e. F � A it means for every frame � �F W R� , . Symbolized as: �A. Accessibility relation properties are the key moment that characterizes the modal logic system type. The fundamental properties that the relation of accessibility can have are the following (see [1, 14]): 1. Reflexivity: s sRs where the world s W� is accessible on its own. 2. Symmetry: s t sRt tRs if world t is accessible from world s then world s is accessible from world t, 3. Transitivity: � s t u sRt tRu sRu if world t is accessible from world s and world u from world t then world u is accessible from world s. It is possible to show [1] that the individual properties of the accessibility relation respect the fundamental axiomatic system of modal logic: ad (1) reflexivity: � A � A (T) ad (2) symmetry: A � � � A (B) ad (3) transitivity: � A � � � A. (4) Now, it is possible to formulate the fundamental system of propositional modal logic as a system created by: 1. the propositional logic axiomatic system 2. the modality distribution axiom: � (A � B) � (�A � �B) (K) 3. the modal interference rule of necessity: and possibly for derivations the inference rule can be used: A modal logic axiomatic system determined in this way is symbolized in the literature as a fundamental system K ac- cording to the characteristic modal axiom. Some other used axiomatic systems of modal propositional logic will be dem- onstrated in the following table. Every type of modal logic is characterized by the set of modal logic axioms. There exists an unambiguous relation between the modal logic axiom and the property of an accessibility relation [14] – see Table 1. The modal logic S4 will be at the center of our attention. It has been shown that the connective � can be defined by using a relationship A � �def � � A and considerations of the connective � can be transferred to similar considerations of the connective �. Symmetrically to the axiom ( T ): � A � A an axiom A � �A exists. In this paper, modal logic will be proposed for design pro- cess formalization. The modal logic worlds will represent individual stages (or steps) of the design process and the rela- tion of accessibility will represent the transition between these stages. 4 © Czech Technical University Publishing House http://ctn.cvut.cz/ap/ Acta Polytechnica Vol. 43 No. 5/2003 X Y� X � Y . X X 3 Design space and metamodel theory In general, the design process is not a simple, “straightfor- ward” mapping coming from the object specification to the field of design object attributes. On the contrary, the design process consists of gradual discrete steps. The design process can branch out, because the designer can choose a transition to several steps. Moreover, one part of the specification can be a set of conditions, which must be valid in every step or there are some optional limits that can be used. These requirements cannot be described by any classical logic. For this reason, modal logic was suggested for design process description. The reasons were based on the described design process char- acteristics – individual discrete steps, design process branch- ing, respecting necessity or possibility types of knowledge. We will try to show in the following text that modal logic as it was determined in above with its accessibility relation and connec- tives of necessity and possibility is an appropriate apparatus for formalizing the given types of design process. A set of accessible worlds W was introduced in the modal logic. Each world was represented by a finite set of valid formulas using mapping V. The individual worlds were con- nected through the relation of accessibility R. A modal logic was built as a formal system based on a formal language, logical axioms and inference rules. The mutual connection between these two systems a design process based on a meta- model theory [3, 4, 5] and modal logic-will be shown in this paper. Definition 1: The formalized metamodel T theory (metamodel theory) is a triad � �T J L A� , , , where J theory language represented by modal lo gic syntax, L theory logic represented by the basic axio- matic system of modal logic, A proper theory axioms. This definition comes from the basic determination of for- malized theory. One part of this theory is a system of proper theory axioms that enables logic axioms of a formalized theory deductive system to be enriched. Proper metamodel theory axioms represent specification of the functional and other attributes of designed objects. Definition 2: Metamodel Mi will be a world w W ii , , , ,0 1 2 � in the sense of modal logic. It was shown above that the system of modal logic worlds is used for interpretation of modal logic formulas. Each world is characterized by formulas of the world evaluation. The metamodel was characterized using a finite set of specifica- tions and attributes of the designed object. Definition 3: The set of metamodels M0, M1, …, Mm, …, will be under- stood as a non-empty set w W i mi , , , , , ,0 1 2 � � of worlds of modal logic where Mi is represented by the world wi for all i. Each world is represented by a set of modal logic formulas. Functional and other design object attributes that represent the object specification are part of the world that represents the metamodel M0 (object specification). The indi- vidual modal logic worlds represent elements of the set of metamodels. Logic axioms of modal logic and proper design axioms form one part of the metamodel theory [3]. Definition 4: The design space over the set of metamodels is a couple of worlds w W i mi , , , , , ,0 1 2 � � and the accessibility rela- tion R (R � W � W ) of modal logic. The design space ensures the possibility to test the set of all metamodels accessible from one of the metamodels, e.g., from a metamodel M0 – of the initial specification. Defi- nition 4 ensures that each design space can be described by a frame F: � �F W R� , , where W represents the set of metamodels, R � W � W characterizes the accessibility relation be- tween individual metamodels. The definition ensures that only those metamodels which are represented in the frame � �F W R� , are concerned in the design. Their connection is represented by the accessibility re- lation R. Definition 5: Accessibility relation R of the design space is reflexive and transitive. The definition comes from a design reality. It is assumed that all conclusions derived in one metamodel (in one design stage) are usable in this particular step (reflexivity). Similarly, conclusions derived in a transition from one design stage to another are also usable in the following design stages (transi- tivity). The other property of the relation of accessibility – symmetry – does not have a practical sense here, so it is not considered. This would mean that the conclusions created in the subsequent steps would be usable in the previous ones, © Czech Technical University Publishing House http://ctn.cvut.cz/ap/ 5 Acta Polytechnica Vol. 43 No. 5/2003 System symbol Accessibility relation property Axioms T s sRs (T): � A � A B s sRs (T): � A � A �s t sRt tRs (B): A � � � A S4 s sRs (T): � A � A � �s t u sRt tRu sRu (4): � A � � �A S5 s sRs (T): � A � A �s t sRt tRs (B): A � � � A � �s t u sRt tRu sRu (4): � A � � �A Table 1: Connection between accessibility relation properties and modal logic axioms which does not correspond with reality. In this case, the acces- sibility relation would cease to represent the basic principle of design process – evolutionary design process. As the accessi- bility relation of the design space is determined design system can be defined as follows. Definition 6: The design system will be understood as a modal logic of type S4. The definition only formulates the facts given in defini- tion 5 in an actual notation used for modal logic type names according to Table 1. An accessibility relation of modal logic of S4 type is characterized by the transitivity and reflexivity property. It has been shown that the characteristic properties of the respective accessibility relation which models the actual de- sign course are the reason for choosing modal logic type S4 for design modeling. The design proceeds gradually from one step to another and everything that was valid in the previous step is transitively used in the subsequent steps (a design can be returned by rejecting the following step, i.e. by exemption of a world from the design process). Similarly, it is true that the properties valid in one step are usable in that step (reflexivity). The given definitions enable us to use the modal logic apparatus for design process formalization – modalities �p and �p respectively, can be used. The most common way of informal interpretation of these formulas is “it must be true in the whole design” or “it will be true somewhere in the design”. A number of definitions have been formulated and a number of theorems that set conditions for validity of the formulas of the formalized T theory have been formulated and proved in our previous work [7]. Let us introduce only a fundamental theorem with the main idea of the proof. Theorem: 1. If in formula f of a metamodel M ii, , , , 0 1 2 � there are no modal connectives, then the validity of formula f validity will be determined as follows: Let us suppose that formula f of metamodel Mi is invalid and let us check recursively whether this assumption is kept even for the subformulas f of the metamodel Mi, or even to the level of atoms. If some logical conflict in the validity of the subformulas occurs during the evalua- tion, then formula f is valid, while it is not valid in the opposite case. 2. If a formula f of a metamodel Mi contains some modal connectives then we proceed as in paragraph 1 with the following exceptions: a. If validity of formula �p is assumed then p must be valid in all metamodels accessible from the tested metamodel Mi. b. If invalidity of formula � p is assumed then � p must be valid in all metamodels accessible from the tested metamodel Mi. c. If invalidity of formula �p is assumed then at least one accessible model from the tested meta- model Mi in which p is not valid must exist. d. If validity of formula � p is assumed then at least one metamodel accessible from the tested meta- model Mi in which p is valid must exist. Proof: Validity of the first part of the theorem follows from the assumption of the consistency of modal logic type S4. This means that if some invalidity of a modal logic formula is as- sumed, then the proof of the contradiction in the subformula validity implies validity of this formula. The second part of the theorem comes from the principle of formula evaluation using modal connectives, from the assumption of consistency of modal logic system S4 and from the theorems published in [1]. The theorem can be understood as an algorithm for for- mula evaluation in a given interpretation. The axiomatic sys- tem and derivation modal logic S4 rules will be used for the design process model determined by the previous definitions. In the axiomatic system S4 several useful theorems can be proved [1, 14]. 4 Conclusion In this article one of the possibilities of a design process description using the modal logic formalism has been dem- onstrated. Modal logic serves as a good means for standard types of design processes (the examples were published in [7]). However, the definition of the metamodel elements set by means of modal logic need not always be so simple and direct. It will be necessary to add also methods, which are capable of testing whether the found solutions actually re- flect the given specification to the deduction methods of the modal logic. Some inconsistencies can also appear during design process. It seems abduction can be a possible appro- priate formal tool [13]. The idea of design theory evokes again a new research in the field of design process description and simulation: synthesis-related methods [8], set-theoretic models [10], syn- thesis design process model [9], general design theory [6], object-oriented approach [11]. It is a question which line of thoughts will be the basis for a true “Common Design Theory”? Acknowledgements This research has been supported by GACR grant No. 102/01/0763 References [1] Chellas, B. F.: Modal Logic: An Introduction. Cambridge University Press, 1980. [2] Suh, N. P.: The Principles of Design. New York: Oxford University Press, 1990. [3] Tomiyama, T., Yoshikawa, H.: Extended General Design Theory. In: Design Theory for CAD (Yoshikawa, H, War- man, E., A. eds.), Proc. of the IFIP WG 5.2 Working Conf. on Design Theory for CAD, IFIP, Tokyo, 1987, p. 95–130. [4] Tomiyama, T.: General Design Theory and its Extension and Applications. In: Universal Design Theory, (Grabowski, H., Rude, S., Grein, G.), Aachen: Shaker Verlag, 1998, p. 25– 46. [5] Akman, V., ten Hagen, P., J., Tomiyama, T.: A Funda- mental and Theoretical Framework for an Intelligent CAD 6 © Czech Technical University Publishing House http://ctn.cvut.cz/ap/ Acta Polytechnica Vol. 43 No. 5/2003 System. Computer Aided Design, Vol. 22, No. 6, July/Au- gust 1990. [6] Reich, Y.: A Critical Review of General Design Theory. Re- search in Engineering Design, Vol. 7, No. 1, 1995, p. 1–18. [7] Jelínek, I: Method for Design Process Description. 6th Inter- national Design Conference Design 2000, Dubrovnik (Croatia), May 2000, p. 107–112. [8] Tsumaya, A., Takeda, H., Tomiyama, T.: A Synthesis-re- lated Analysis Method of Design Protocol. In: Proceedings of the 12th International Conference on Engineering Design (Lindeman, Birkhofer eds.), ICED’99, Munich, 1999, p. 1949–1952. [9] Washio, T., Hew, K. P., Tomiyama, T., Umeda, Y.: The Modelling of Synthesis – from the Viewpoints of Mathematical Logic. In: Proceedings of the 12th International Confer- ence on Engineering Design. (Lindeman, Birkhofer eds.), ICED’99, Munich, 1999, p. 1219–1222. [10] Zeng, Y., Gu, P.: A Set-theoretic Model of Design Process. In: Proceedings of the 12th International Conference on En- gineering Design (Lindeman, Birkhofer eds.), ICED’99, Munich, 1999, p. 1117–1120. [11] Pavkovič, N., Marjanovič, D.: Entities in the Object-Oriented Design Process Model. 6th International Design Conf. De- sign 2000, Dubrovnik (Croatia), May 2000, p. 29–34. [12] Smets, P., Mamdani, E. H., Dobois, D., Prade, H.: Non- -Standard Logics for Automated Reasoning. Academic Press, London, 1988. [13] Takeda, H.: Abduction for Design. In: Proceedings of the IFIP TC5/WG 5.2 Workshop of Formal Design Methods for CAD, (Gero, J., S., Tyugu, E. eds.), Tallin, 1994, p. 221–244. [14] Hughes, G. E., Cresswell, M. J.: Introduction to Modal Logic. London: Methuen, 1982. Prof. Dr. Ivan Jelínek phone: +420 224 357 214 fax: +420 224 923 325 email.: jelinek@fel.cvut.cz Department of Computer Science and Engineering Czech Technical University in Prague Faculty of Electrical Engineering Karlovo nám. 13 121 35 Prague 2, Czech Republic © Czech Technical University Publishing House http://ctn.cvut.cz/ap/ 7 Acta Polytechnica Vol. 43 No. 5/2003