It is proved in this paper that checking a timed automaton M with respect to a linear duration property D can be done by investigating only the integral timed states of M. An equivalence relation is introduced in this...It is proved in this paper that checking a timed automaton M with respect to a linear duration property D can be done by investigating only the integral timed states of M. An equivalence relation is introduced in this paper to divide the infinite number of integral timed states into finite number of equivalence classes. Based on this, a method is proposed for checking whether M satisfies D. In some cases, the number of equivalence classes is too large for a computer to manipulate. A technique for reducing the search-space for checking linear duration property is also described. This technique is more suitable for the case in this paper than those in the literature because most of those techniques are designed for reachability analysis.展开更多
This paper puts forward'a general architecture model of CPDL Interpreter,profiles the logical structure of the modules, and analyses the burden distri-bution among the interpreter units. The work has significance ...This paper puts forward'a general architecture model of CPDL Interpreter,profiles the logical structure of the modules, and analyses the burden distri-bution among the interpreter units. The work has significance in developing practical interpreter products.展开更多
This paper presents a declarative semantics of compositional inheritancein an object-oriented logic programming' framework wit h explicit exceptions,based on the iterated least Aspoint semantics to normal logic pr...This paper presents a declarative semantics of compositional inheritancein an object-oriented logic programming' framework wit h explicit exceptions,based on the iterated least Aspoint semantics to normal logic programs. Tak-ing logic objects with exceptions as a ldnd of nonmonotonic theory, the nonmonotonicity of inheritance is achieved, which is of importance for modelingincomplete knowledge and requirement specffications in both artificial intelli-gence and softwa-re engineering.展开更多
This paper presents a framework called logical knowledge object (LKO),which is taken as a basis of the dependable development of knowledge based systems(KBSs). LKO combines logic programming and object-oriented progra...This paper presents a framework called logical knowledge object (LKO),which is taken as a basis of the dependable development of knowledge based systems(KBSs). LKO combines logic programming and object-oriented programming paradigms, where objects are viewed as abstractions with states,constraints, behaviors and inheritance. The operational semantics defined in the style of natural semantics is simple and clear. A hybrid knowledge represen-tation amalgamating rule, frame, semantic network and blackboard is available for both most structured and flat knowledge. The management of knowledge bases has been formally specified. Accordingly, LKO is well suited for the formal representation of knowledge and requirements of KBSs. Based on the framework, verification techniques are also explored to enhance the analysis of requirement specifications and the validation of KBSs. In addition, LKO pro-vides a methodology for the development of KBSs, applying the concepts of rapid prototyping and top-down design to deal with changing and incomplete requirements, and to provide multiple abstract models of the domain, where formal methods might be used at each abstract level.展开更多
In this paper we propose a novel scheme for scheduling divisible task onparallel processors connected by system interconnection network with arbitrary topology. Thedivisible task is a computation that can be divided i...In this paper we propose a novel scheme for scheduling divisible task onparallel processors connected by system interconnection network with arbitrary topology. Thedivisible task is a computation that can be divided into arbitrary independent subtasks solvedin parallel. Our model takes into consideration communication initial time and communicationdelays between processors. Moreover, by constructing the corresponding Network SpanningTree (NST) for a network, our scheme can be applied to all kinds of network topologies. Wepresent the concept of Balanced Task Distribution Tree and use it to design the Equation SetCreation Algorithm in which the set of linear equations is created by traversing the NST inpost-order. After solving the created equations, we get the optimal task assignment scheme.Experiments confirm the applicability of our scheme in real-life situations.展开更多
摘要It is proved in this paper that checking a timed automaton M with respect to a linear duration property D can be done by investigating only the integral timed states of M. An equivalence relation is introduced in this paper to divide the infinite number of integral timed states into finite number of equivalence classes. Based on this, a method is proposed for checking whether M satisfies D. In some cases, the number of equivalence classes is too large for a computer to manipulate. A technique for reducing the search-space for checking linear duration property is also described. This technique is more suitable for the case in this paper than those in the literature because most of those techniques are designed for reachability analysis.
摘要This paper puts forward'a general architecture model of CPDL Interpreter,profiles the logical structure of the modules, and analyses the burden distri-bution among the interpreter units. The work has significance in developing practical interpreter products.
摘要This paper presents a declarative semantics of compositional inheritancein an object-oriented logic programming' framework wit h explicit exceptions,based on the iterated least Aspoint semantics to normal logic programs. Tak-ing logic objects with exceptions as a ldnd of nonmonotonic theory, the nonmonotonicity of inheritance is achieved, which is of importance for modelingincomplete knowledge and requirement specffications in both artificial intelli-gence and softwa-re engineering.
摘要This paper presents a framework called logical knowledge object (LKO),which is taken as a basis of the dependable development of knowledge based systems(KBSs). LKO combines logic programming and object-oriented programming paradigms, where objects are viewed as abstractions with states,constraints, behaviors and inheritance. The operational semantics defined in the style of natural semantics is simple and clear. A hybrid knowledge represen-tation amalgamating rule, frame, semantic network and blackboard is available for both most structured and flat knowledge. The management of knowledge bases has been formally specified. Accordingly, LKO is well suited for the formal representation of knowledge and requirements of KBSs. Based on the framework, verification techniques are also explored to enhance the analysis of requirement specifications and the validation of KBSs. In addition, LKO pro-vides a methodology for the development of KBSs, applying the concepts of rapid prototyping and top-down design to deal with changing and incomplete requirements, and to provide multiple abstract models of the domain, where formal methods might be used at each abstract level.
摘要In this paper we propose a novel scheme for scheduling divisible task onparallel processors connected by system interconnection network with arbitrary topology. Thedivisible task is a computation that can be divided into arbitrary independent subtasks solvedin parallel. Our model takes into consideration communication initial time and communicationdelays between processors. Moreover, by constructing the corresponding Network SpanningTree (NST) for a network, our scheme can be applied to all kinds of network topologies. Wepresent the concept of Balanced Task Distribution Tree and use it to design the Equation SetCreation Algorithm in which the set of linear equations is created by traversing the NST inpost-order. After solving the created equations, we get the optimal task assignment scheme.Experiments confirm the applicability of our scheme in real-life situations.