Ambient logics have been proposed to describe properties for mobile agentswhich may evolve over time as well as space. This paper takes a predicate-based approach toextending an ambient logic with recursion, yielding ...Ambient logics have been proposed to describe properties for mobile agentswhich may evolve over time as well as space. This paper takes a predicate-based approach toextending an ambient logic with recursion, yielding a predicate μ-calculus in which fixpointformulas are formed using predicate variables. An algorithm is developed for model checkingfinite-control mobile ambients against formulas of the logic, providing the first decidabilityresult for model checking a spatial logic with recursion.展开更多
Semi-input-memory finite automata,a kind of finite automata introduced by the first author of this paper for studying error propagation ,are a generalization of inputmemory finite automata ,by appending an autonomous ...Semi-input-memory finite automata,a kind of finite automata introduced by the first author of this paper for studying error propagation ,are a generalization of inputmemory finite automata ,by appending an autonomous finite automation component .In this paper,we give a characterization of the structure of weakly invertible semi-input-memory finite automata with delay 1,in which the state graph of each autonomous finite automation is cycle,From a result on mutual invertibility of finite automata obtained by th authors recently,it leads to a characerization of the structure of feedfoward inverse finite automata with delay 1.展开更多
Ra, Rb transformations were successfully applied to establish invertibility theory for linear and quasi-linear finite automata over finite fields. In aprevious paper, the authors generalized R., Rb transformations to ...Ra, Rb transformations were successfully applied to establish invertibility theory for linear and quasi-linear finite automata over finite fields. In aprevious paper, the authors generalized R., Rb transformations to deal with nonlinear memory finite automata, and gave sufficient conditions for weak inverse andfor weakly invertible memory finite automata and inversion processes concerned;methods by transformation to generate a kind of nonlinear memory finite automatasatisfying one of these sufficient conditions were also given. This paper extends theconcepts, methods and results to general finite automata, in which states consist offinite input history, finite output history and finite 'inner state' history.展开更多
Java Beans is a standard for software components. For checkingthe consistency of the Java Beaus semantic constraints with its implementation,this paper proposes a formal Java Beaus Description Language (JBDL) to speci...Java Beans is a standard for software components. For checkingthe consistency of the Java Beaus semantic constraints with its implementation,this paper proposes a formal Java Beaus Description Language (JBDL) to specifycomponent semantic constraints. The JBDL logic is based on many sorted firstorder logic and Computation Tree Logic (CTL), with extension of some facilities inspecifying object oriented features. A framework for dynamic checking Java Beaussemantic constraines in JBDL form is described in this paper and some experimentalresults are showed by examples.展开更多
In this paper, to model check real-time value-passing systems, a formallanguage Timed Symbolic Transition Graph and a logic system named Timed Predicate μ-Calculus areproposed. An algorithm is presented which is loca...In this paper, to model check real-time value-passing systems, a formallanguage Timed Symbolic Transition Graph and a logic system named Timed Predicate μ-Calculus areproposed. An algorithm is presented which is local in that it generates and investigates thereachable state space in top-down fashion and maintains the partition for time evaluations as coarseas possible while on-the-fly instantiating data variables. It can deal with not only data variableswith finite value domain, but also the so called data independent variables with infinite valuedomain. To authors knowledge, this is the first algorithm for model checking timed systemscontaining value-passing features.展开更多
A modal logic for describing temporal as well as spatial properties of mobileprocesses, expressed in the asynchronous π-calculus, is presented. The logic has recur-sive constructs built upon predicate-variables. The ...A modal logic for describing temporal as well as spatial properties of mobileprocesses, expressed in the asynchronous π-calculus, is presented. The logic has recur-sive constructs built upon predicate-variables. The semantics of the logic is establishedand shown to be monotonic, thus guarantees the existence of fixpoints. An algorithm isdeveloped to automatically check if a mobile process has properties described as formulasin the logic. The correctness of the algorithm is proved.展开更多
A graphical notation for the propositionalμ-calculus, called modal graphs, ispresented. It is shown that both the textual and equational presentations of theμ-calculus canbe translated into modal graphs. A model che...A graphical notation for the propositionalμ-calculus, called modal graphs, ispresented. It is shown that both the textual and equational presentations of theμ-calculus canbe translated into modal graphs. A model checking algorithm based on such graphs is proposed.The algorithm is truly local in the sense that it only generates the parts of the underlyingsearch space which are necessary for the computation of the final result. The correctness of thealgorithm is proven and its complexity analysed.展开更多
文摘Ambient logics have been proposed to describe properties for mobile agentswhich may evolve over time as well as space. This paper takes a predicate-based approach toextending an ambient logic with recursion, yielding a predicate μ-calculus in which fixpointformulas are formed using predicate variables. An algorithm is developed for model checkingfinite-control mobile ambients against formulas of the logic, providing the first decidabilityresult for model checking a spatial logic with recursion.
文摘Semi-input-memory finite automata,a kind of finite automata introduced by the first author of this paper for studying error propagation ,are a generalization of inputmemory finite automata ,by appending an autonomous finite automation component .In this paper,we give a characterization of the structure of weakly invertible semi-input-memory finite automata with delay 1,in which the state graph of each autonomous finite automation is cycle,From a result on mutual invertibility of finite automata obtained by th authors recently,it leads to a characerization of the structure of feedfoward inverse finite automata with delay 1.
文摘Ra, Rb transformations were successfully applied to establish invertibility theory for linear and quasi-linear finite automata over finite fields. In aprevious paper, the authors generalized R., Rb transformations to deal with nonlinear memory finite automata, and gave sufficient conditions for weak inverse andfor weakly invertible memory finite automata and inversion processes concerned;methods by transformation to generate a kind of nonlinear memory finite automatasatisfying one of these sufficient conditions were also given. This paper extends theconcepts, methods and results to general finite automata, in which states consist offinite input history, finite output history and finite 'inner state' history.
文摘Java Beans is a standard for software components. For checkingthe consistency of the Java Beaus semantic constraints with its implementation,this paper proposes a formal Java Beaus Description Language (JBDL) to specifycomponent semantic constraints. The JBDL logic is based on many sorted firstorder logic and Computation Tree Logic (CTL), with extension of some facilities inspecifying object oriented features. A framework for dynamic checking Java Beaussemantic constraines in JBDL form is described in this paper and some experimentalresults are showed by examples.
文摘In this paper, to model check real-time value-passing systems, a formallanguage Timed Symbolic Transition Graph and a logic system named Timed Predicate μ-Calculus areproposed. An algorithm is presented which is local in that it generates and investigates thereachable state space in top-down fashion and maintains the partition for time evaluations as coarseas possible while on-the-fly instantiating data variables. It can deal with not only data variableswith finite value domain, but also the so called data independent variables with infinite valuedomain. To authors knowledge, this is the first algorithm for model checking timed systemscontaining value-passing features.
文摘A modal logic for describing temporal as well as spatial properties of mobileprocesses, expressed in the asynchronous π-calculus, is presented. The logic has recur-sive constructs built upon predicate-variables. The semantics of the logic is establishedand shown to be monotonic, thus guarantees the existence of fixpoints. An algorithm isdeveloped to automatically check if a mobile process has properties described as formulasin the logic. The correctness of the algorithm is proved.
文摘A graphical notation for the propositionalμ-calculus, called modal graphs, ispresented. It is shown that both the textual and equational presentations of theμ-calculus canbe translated into modal graphs. A model checking algorithm based on such graphs is proposed.The algorithm is truly local in the sense that it only generates the parts of the underlyingsearch space which are necessary for the computation of the final result. The correctness of thealgorithm is proven and its complexity analysed.
