This article extends the foundational work of Wang and Wang on modal logic over lattices.Building upon their framework using polyadic modal logic with binary modalities<sup>and<inf>under standard Kripke se...This article extends the foundational work of Wang and Wang on modal logic over lattices.Building upon their framework using polyadic modal logic with binary modalities<sup>and<inf>under standard Kripke semantics to axiomatize lattice structures,we focus on the modal characterization of bounded lattices and their extensions relevant to logical systems.By introducing nullary modalities 1(maximum element)and 0(minimum element),we first establish a modal axiomatic system for bounded lattices.Subsequently,we provide pure formula characterizations of complementation and orthocomplementation relations in lattices,along with corresponding completeness results.As key applications,we present modal characterizations of fundamental logical algebraic structures:Boolean algebras,orthomodular lattices,and Heyting algebras.The last section develops novel axiomatization results for atomic lattices and atomless lattices.Throughout this work,all axiomatic systems are shown to be strongly complete via pureformula extensions,demonstrating how hybrid modal languages with nullary operators can uniformly capture boundary elements,complementation properties,and latticetheoretic operations central to both classical and nonclassical logics.展开更多
The standard Kripke semantics of epistemic logics has been applied successfully to reasoning communication protocols under the assumption that the network is not hostile. This paper introduces a natural semantics of K...The standard Kripke semantics of epistemic logics has been applied successfully to reasoning communication protocols under the assumption that the network is not hostile. This paper introduces a natural semantics of Kripke semantics called knowledge structure and, by this kind of Kripke semantics, analyzes communication protocols over hostile networks, especially on authentication protocols. Compared with BAN-like logics, the method is automatically implementable because it operates on the actual definitions of the protocols, not on some difficult-to-establish justifications of them. What is more, the corresponding tool called SPV (Security Protocol Verifier) has been developed. Another salient point of this approach is that it is justification-oriented instead of falsification-oriented, i.e. finding bugs in protocols.展开更多
During the last decade, Model Checking has proven its efficacy and power in circuit design, network protocol analysis and bug hunting. Recent research on automatic verification has shown that no single model-checking ...During the last decade, Model Checking has proven its efficacy and power in circuit design, network protocol analysis and bug hunting. Recent research on automatic verification has shown that no single model-checking technique has the edge over all others in all application areas. So, it is very difficult to determine which technique is the most suitable for a given model. It is thus sensible to apply different techniques to the same model. However, this is a very tedious and time-consuming task, for each algorithm uses its own description language. Applying Model Checking in software design and verification has been proved very difficult. Software architectures （SA） are engineering artifacts that provide high-level and abstract descriptions of complex software systems. In this paper a Direct Model Checking （DMC） method based on Kripke Structure and Matrix Algorithm is provided. Combined and integrated with domain specific software architecture description languages （ADLs）, DMC can be used for computing consistency and other critical properties.展开更多
The process of understanding natural language can be viewed as the process of model construction. This paper? employing Kripke frame for intuitionistic logic semantics as the implement of model construction for natura...The process of understanding natural language can be viewed as the process of model construction. This paper? employing Kripke frame for intuitionistic logic semantics as the implement of model construction for natural language, introduces a method of incremental model construction.展开更多
基金supported by China Postdoctoral Science Foundation(2024M750225).
文摘This article extends the foundational work of Wang and Wang on modal logic over lattices.Building upon their framework using polyadic modal logic with binary modalities<sup>and<inf>under standard Kripke semantics to axiomatize lattice structures,we focus on the modal characterization of bounded lattices and their extensions relevant to logical systems.By introducing nullary modalities 1(maximum element)and 0(minimum element),we first establish a modal axiomatic system for bounded lattices.Subsequently,we provide pure formula characterizations of complementation and orthocomplementation relations in lattices,along with corresponding completeness results.As key applications,we present modal characterizations of fundamental logical algebraic structures:Boolean algebras,orthomodular lattices,and Heyting algebras.The last section develops novel axiomatization results for atomic lattices and atomless lattices.Throughout this work,all axiomatic systems are shown to be strongly complete via pureformula extensions,demonstrating how hybrid modal languages with nullary operators can uniformly capture boundary elements,complementation properties,and latticetheoretic operations central to both classical and nonclassical logics.
基金the reviewers.an d the trem endous kind help from the editors.This work was supported by the National Natural Science Foundation of China(Grant Nos.64096327,10410638 , 60473004)Germ an Research Foundation(Grant No.446 CHV1 13/240/0.1) Guangdong Provincial Natural Science Foundation(Grant No.04205407)
文摘The standard Kripke semantics of epistemic logics has been applied successfully to reasoning communication protocols under the assumption that the network is not hostile. This paper introduces a natural semantics of Kripke semantics called knowledge structure and, by this kind of Kripke semantics, analyzes communication protocols over hostile networks, especially on authentication protocols. Compared with BAN-like logics, the method is automatically implementable because it operates on the actual definitions of the protocols, not on some difficult-to-establish justifications of them. What is more, the corresponding tool called SPV (Security Protocol Verifier) has been developed. Another salient point of this approach is that it is justification-oriented instead of falsification-oriented, i.e. finding bugs in protocols.
文摘During the last decade, Model Checking has proven its efficacy and power in circuit design, network protocol analysis and bug hunting. Recent research on automatic verification has shown that no single model-checking technique has the edge over all others in all application areas. So, it is very difficult to determine which technique is the most suitable for a given model. It is thus sensible to apply different techniques to the same model. However, this is a very tedious and time-consuming task, for each algorithm uses its own description language. Applying Model Checking in software design and verification has been proved very difficult. Software architectures （SA） are engineering artifacts that provide high-level and abstract descriptions of complex software systems. In this paper a Direct Model Checking （DMC） method based on Kripke Structure and Matrix Algorithm is provided. Combined and integrated with domain specific software architecture description languages （ADLs）, DMC can be used for computing consistency and other critical properties.
基金This paper was supported by the National Natural Science Foundation of China and the National '863' Hi-Tech Programme of China.
文摘The process of understanding natural language can be viewed as the process of model construction. This paper? employing Kripke frame for intuitionistic logic semantics as the implement of model construction for natural language, introduces a method of incremental model construction.
