Author name cluster

Zhenhua Duan

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

31 papers

2 author rows

EAAI Journal 2026 Journal Article

Engineering application of non-dominated sorting genetic algorithm III: Multi-objective optimization of ultra-high performance concrete for diverse scenarios

Wei Zhang
Zhenhua Duan
Yuqing Wu
Chao Liu
Yizhou Yao
Ahmed Nasr
Qingmei Yang
Huiyu Xia

This study addresses the technical limitations of conventional mix design methods for ultra-high performance concrete (UHPC) concerning multi-objective synergistic optimization and diverse scenarios adaptability. Leveraging 2824 experimental data points, a comprehensive prediction system was established for mechanical properties, workability and durability. The prediction performance of ten machine learning algorithms was systematically evaluated, and the SHapley Additive exPlanations (SHAP) method was used to elucidate the influence mechanism of crucial features. Furthermore, a comprehensive collaborative optimization framework for UHPC under typical engineering scenarios was developed by integrating the non-dominated sorting genetic algorithm III (NSGA-III) with the technique for order preference by similarity to ideal solution (TOPSIS) decision-making model, and visualization technology was integrated to construct a graphical user interface (GUI) system. The results demonstrate that the NSGA-III algorithm achieved continuous hypervolume (HV) improvement within 500 generations, while the spacing indicator decreased rapidly in the initial iterations, confirming its capability to approximate the actual Pareto front through adaptive crossover-mutation strategies and elitism preservation. The developed ‘data driven - performance prediction - multi objective optimization - decision analysis' technical system, provides a quantifiable and scalable solution for addressing multi-objective optimization challenges in engineering materials.

AAAI Conference 2026 Conference Paper

T4NMTD: Transition-Centric Reinforcement Learning for Non-Markovian Task Decomposition

Ruixuan Miao
Xu Lu
Cong Tian
Bin Yu
Zhenhua Duan

Non-Markovian Tasks (NMTs) are distinguished by their dependence on long-term memory and state-dependent dynamics, setting them apart from the traditional Markovian models typically employed in Reinforcement Learning (RL). NMTs not only suffer from reward sparseness but also rely on historical information, making their resolution considerably more challenging. In this paper, we propose a novel RL framework T4NMTD (Transition-centric framework for NMT Decomposition), designed specifically for learning NMTs which are specified by temporal logic. The core of T4NMTD is a task decomposition mechanism along with a parallel training approach for NMTs. An NMT is first decomposed as basic units based on the transitions of the automata which are derived from temporal logic formulae. The units are then modularized into sub-tasks according to their semantic similarity under logical interpretation. The training strategy of T4NMTD adopts a dual-level structure: the high-level learns to shape the boundaries and coordinate arrangement of the sub-tasks from a global perspective, while the low-level learns those sub-tasks in parallel. In addition, we invent a dynamic policy intervention scheme to mitigate the policy myopic issue during parallel training. A comprehensive evaluation is conducted on benchmark problems with respect to various metrics. The experimental results demonstrate that T4NMTD effectively addresses NMTs, achieving significant performance improvements compared with related studies.

PDF Details DOI

TCS Journal 2025 Journal Article

Improved SARSA and DQN algorithms for reinforcement learning

Guangyu Yao
Nan Zhang
Zhenhua Duan
Cong Tian

Reinforcement learning is a branch of machine learning in which an agent interacts with an environment to learn optimal actions that maximize cumulative rewards. This paper aims to enhance the SARSA and DQN algorithms in four key aspects: the ε-greedy policy, reward function, value iteration approach, and sampling probability. The experiments are conducted in three scenarios: path planning, CartPole, and MountainCar. The results show that, in these environments, the improved algorithms exhibit better convergence, higher rewards, and more stable training processes.

TCS Journal 2025 Journal Article

SAT-based bounded model checking for propositional projection temporal logic

Zhenhua Duan
Cong Tian
Nan Zhang
Chaofeng Yu
Mengfei Yang
Jia He

This paper presents a bounded model checking (BMC) approach for propositional projection temporal logic (PPTL). To this end, first PPTL is briefly introduced. Then, bounded semantics of PPTL is defined according to its semantics in logic theory. Further, a reduction method from BMC to SAT is given in detail. In addition, an example is presented to illustrate how the approach works. Finally, miniSAT is employed to solve the SAT based BMC problem by means of verifying RMS algorithm in detail. Our experience shows that SAT based BMC approach for PPTL proposed in the paper is useful and feasible.

TCS Journal 2024 Journal Article

Generating Java code pairing with ChatGPT

Zelong Zhao
Nan Zhang
Bin Yu
Zhenhua Duan

The Large Language Models (LLMs) like ChatGPT 3. 5 have created a new era of automatic code generation. However, the existing research primarily focuses on generating simple code based on datasets (such as HumanEval, etc.). Most of approaches pay less attention to complex and practical code generation. Therefore, in this paper, we propose a new approach called “Xd-CodeGen” which can be used to generate large scale Java code. This approach is composed of four phases: requirement analysis, modeling, code generation, and code verification. In the requirement analysis phase, ChatGPT 3. 5 is utilized to decompose and restate user requirements. To do so, a knowledge graph is developed to describe entities and their relationship in detail. Further, Propositional Projection Temporal Logic (PPTL) formulas are employed to define the properties of requirements. In the modeling phase, we use knowledge graphs to enhance prompts and generate UML class and activity diagrams for each sub-requirement using ChatGPT 3. 5. In the code generation phase, based on established UML models, we make use of prompt engineering and knowledge graph to generate Java code. In the code verification phase, a runtime verification at code level approach is employed to verify generated Java code. Finally, we apply the proposed approach to develop a practical Java web project.

TCS Journal 2023 Journal Article

A proof system for unified temporal logic

Nan Zhang
Chaofeng Yu
Zhenhua Duan
Cong Tian

Unified Temporal Logic (UTL) combines all characteristics of traditional Linear Temporal Logic (LTL) and Propositional Projection Temporal Logic (PPTL). It can be used to describe full regular and omega-regular properties, which are often encountered in the field of formal verification. To support formal verification with UTL, this paper proposes a proof system for UTL. First, the syntax and semantics of UTL are briefly introduced. Further, axioms and inference rules are formalized. Besides, a number of theorems are derived and proved to refine the system. Moreover, the soundness and completeness of the proof system are proved in detail. To facilitate the completeness proof, some auxiliary lemmas are introduced and proved in advance. Finally, an example is given to illustrate how to use this proof system for verifying properties of a system.

TCS Journal 2022 Journal Article

PPTL specification mining based on LNFG

Xinya Ning
Nan Zhang
Zhenhua Duan
Cong Tian

A formal specification is a formal description of system requirements, which is a necessity for formal verification. Due to various reasons, some systems lack of formal specifications. Compared with CTL and LTL, Propositional Projection Temporal Logic (PPTL) has a full regular expressive power. Accordingly, a pattern-library-based PPTL specification mining tool PPTLMiner [1] is able to dig out a better expression of system specification. However, there's still some room for improvement in PPTLMiner, such as deep recursion, high time complexity and space complexity, which limit the use of PPTLMiner in practical applications. Therefore, in this paper, a new PPTL specification mining approach based on Labeled Normal Form Graph (LNFG) is proposed and a supporting tool PPTLMiner+ is also developed. Finally, a specification mining example using PPTLMiner+ is given to illustrate the effectiveness and practicality of the new approach. In this example, a typical algorithm in Swarm Intelligence-Bee Colony Algorithm is selected as a target program, and the working order of EmployedBees, OnlookerBees and ScoutBees is obtained using PPTLMiner+. Further, PPTLMiner+ is compared with PPTLMiner as well as the classical linear specification mining tool Texada [2, 3] in terms of time and memory to illustrate the effectiveness and practicability of the proposed method.

TCS Journal 2021 Journal Article

Multi-matching nested relations

Jin Liu
Zhenhua Duan
Cong Tian

Multi-matching nested relation consists of a sequence of linearly ordered positions, call, internal, and return, augmented with one-to-one, one-to-n or n-to-one matching nested edges from call to return. For clarity, inner-call and inner-return are defined in n-to-one and one-to-n matching nested relations respectively. After word encoding by introducing tagged letters, Multi-matching Nested Words (MNWs) are obtained over a tagged alphabet. Then Multi-matching Nested Expression (MNE) and Multi-matching Nested Traceable Automaton (MNTA) are defined over MNWs. The closure properties of languages over MNWs are studied, including union, intersection, concatenation, Kleene-* and complementation. Moreover, nondeterministic MNTAs are as expressive as deterministic ones. Further, a transformation method from MNTAs to MNEs is proposed, where three kinds of labeled arcs are created for different transitions in order for the specific merging strategies. To specify the requirements of multi-matching nested calls and returns, we propose a temporal logic of Multi-matching Nested CAlls and RETurns (MNCARET). The abstract and matched-abstract versions of modalities are considered. For example, abstract-next operator allows a path to jump from a call to the first matched non-internal, which is the inner-call, inner-return or return, in a one-to-n or n-to-one matching relation while matched-abstract-next operator from a call directly to the matched return. We also present an approach to model check MNCARET formulas for the MNTA model, a subset of pushdown automata. This problem is reduced to the emptiness problem of Büchi MNTAs.

TCS Journal 2021 Journal Article

Temporal logic specification mining of programs

Nan Zhang
Bin Yu
Cong Tian
Zhenhua Duan
Xiaoshuai Yuan

This paper proposes a dynamic approach of specification mining for Propositional Projection Temporal Logic (PPTL). To this end, a pattern library is built to collect some common temporal relation among events. Further, several algorithms of specification mining for PPTL are designed. With our approach, PPTL specifications are mined from a trace set of a target program by using patterns in the library. In addition, a specification mining tool PPTLMiner supporting this approach is developed. In practice, given a trace set and user selected patterns, PPTLMiner can capture PPTL specifications of target programs.

TCS Journal 2021 Journal Article

Unified temporal logic

Nan Zhang
Zhenhua Duan
Cong Tian

This paper proposes a new temporal logic named Unified Temporal Logic (UTL). First, the syntax and semantics of UTL are inductively defined. Further, logic laws in UTL are formalized and proved. Moreover, the normal forms of UTL formulas are defined and proved. To illustrate how to describe properties with UTL, an example of an elevator control system is given. In general, UTL combines the characteristics of Linear Temporal Logic (LTL) and Propositional Projection Temporal Logic (PPTL). So properties involving the “until” construct in LTL and the “chop” construct in PPTL can easily be represented in UTL. In addition, both finite and infinite models (intervals) are supported. With UTL, we are able to specify and verify some practical properties which cannot easily be formalized in LTL and PPTL.

TCS Journal 2020 Journal Article

A decision procedure and complete axiomatization for projection temporal logic

Xinfeng Shu
Zhenhua Duan
Hongwei Du

To specify and verify the concurrent and reactive systems with the theorem proving approach, a complete axiomatization is formalized for first order projection temporal logic (PTL) with both finite and infinite time. To this end, PTL is restricted to a finite domain, and the syntax, semantics as well as the axiomatization of PTL are presented. Further, the techniques of labeled normal form and labeled normal form graph of PTL formulas are introduced respectively, with which a decision procedure for quantifier free PTL (QFPTL) formulas is given. Moreover, a generalized labeled normal form graph is defined and employed to transform a quantified PTL formula into its equivalent QFPTL formula. Finally, a decision procedure for PTL is formalized and the completeness of the axiomatic system is proved based on the decidability of PTL formulas.

TCS Journal 2020 Journal Article

A novel approach to verifying context free properties of programs

Nan Zhang
Zhenhua Duan
Cong Tian
Hongwei Du

This paper proposes an approach to verifying context free properties of programs. In this approach, the system to be verified is modeled as a program m in Modeling, Simulation and Verification Language (MSVL), and the desired property is also specified by an MSVL program m ′. Then program m and formula ¬ m ′ are interpreted by means of executing programs m and m ′. If an acceptable execution path is generated, a counterexample is found, otherwise the property is valid. To show how the proposed approach works, an example is given.

TCS Journal 2020 Journal Article

Translating Xd-C programs to MSVL programs

Meng Wang
Cong Tian
Nan Zhang
Zhenhua Duan
Chenguang Yao

C language is one of the most popular languages for software systems. In order to verify safety, reliability and security properties of such systems written in C, a tool UMC4M for runtime verification at code level based on Modeling, Simulation and Verification Language (MSVL) and its compiler MC is employed. To do so, a C program P has to be translated to an MSVL program M and the negation of a desired property Q is also translated to an MSVL program M', then “M and M'” is compiled and executed armed with MC. Whether P violates Q is checked by evaluating whether there exists an acceptable execution of new MSVL program “M and M'”. Therefore, how to translate a C program to an MSVL program is a critical issue. However, in general, C is of complicated structures with goto statement. In this paper, we confine the syntax of C in a suitable subset called Xd-C without loss of expressiveness. Further, we present a translation algorithm from an Xd-C program to an MSVL program based on translation algorithms for expressions and statements. Moreover, the equivalences between expressions and statements involved in Xd-C and MSVL programs are inductively proved. Subsequently, the equivalence between the original Xd-C program and the translated MSVL program is also proved. In addition, the proposed approach has been implemented by a tool called C 2 M. A benchmark of experiments including 13 real-world Xd-C programs is conducted. The results show that C 2 M works effectively.

TCS Journal 2020 Journal Article

Verify heaps via unified model checking

Xu Lu
Zhenhua Duan
Cong Tian
Hongwei Du

This paper addresses the problem of verifying heap evolution properties of pointer programs. To this end, a new unified model checking approach with MSVL (Modeling, Simulation and Verification Language) and PPTLSL is presented. The former is an executable subset of PTL (Projection Temporal Logic) while the latter is an extension of PPTL (Propositional Projection Temporal Logic) with separation logic. MSVL is used to model pointer programs, and PPTLSL to specify heap evolution properties. Technically, on one hand, models of MSVL programs are characterized by Normal Form Graphs (NFGs). On the other hand, PPTLSL is equisatisfiably reduced to its subset which can reuse the decision procedure of PPTL. Our technique is able to deal with a variety of pointer structures such as linked lists and composite structures. In addition, we implement a prototype tool by using an SMT solver as the verification engine in order to demonstrate our approach.

TCS Journal 2019 Journal Article

Index set expressions can represent temporal logic formulas

Zhenhua Duan
Cong Tian
Nan Zhang
Qian Ma
Hongwei Du

In Temporal Logic (TL), a well-formed formula is generally formed by applying rules of its syntax finitely many times. However, under some circumstances, although formulas such as ones expressed by index set expressions, are constructed via applying rules of the syntax infinitely many times, they are possibly still well-formed since their equivalent concise syntax formulas can be found. With this motivation, this paper investigates the relationship between formulas specified by index set expressions and concise syntax by means of fixed-point approach. Firstly, we present two kinds of formulas, namely ⋁ i ∈ N 0 ◯ i Q and ⋁ i ∈ N 0 Q i, and prove they are indeed well-formed by proving they are equivalent to formulas ◇Q and Q ⁎ respectively. Further, we generalize ⋁ i ∈ N 0 ◯ i Q to ⋁ i ∈ N 0 P ( i ) ∧ ◯ i Q and explore the least and greatest fixed-points of an abstract equation X ≡ Q ∨ P ∧ ◯ X. Based on these, some well-formed special instances of ⋁ i ∈ N 0 P ( i ) ∧ ◯ i Q are obtained. Besides, with the index set expression technique, we equivalently represent ‘ U ’ (strong until) and ‘ W ’ (weak until) constructs of propositional Linear Temporal Logic (LTL) within Propositional Projection Temporal Logic (PPTL).

TCS Journal 2019 Journal Article

Model checking of pushdown systems for projection temporal logic

Liang Zhao
Xiaobing Wang
Zhenhua Duan

In this paper, we study the model checking problem of pushdown systems for projection temporal logic (PTL), an interval-based temporal logic that is as expressive as the full regular languages. For this, we provide an algorithm to decide whether a pushdown system, determined by a pushdown automaton, satisfies a desired logic property, by using relevant automata notations and operations. The algorithm terminates in exponential time for normal PTL properties, i. e. properties specified as normal PTL formulas. To show the lower bound of complexity of the model checking problem, we also construct a polynomial-time reduction from the acceptance problem of a linearly bounded alternating Turing machine. As a result, the model checking problem of pushdown systems for normal PTL properties is EXPTIME-complete.

TCS Journal 2019 Journal Article

Model checking open systems with alternating projection temporal logic

Cong Tian
Zhenhua Duan

To specify properties of open systems with interval based temporal logics, Alternating Projection Temporal Logic (APTL) is proposed by introducing Concurrent Game Structures (CGS) to Propositional Projection Temporal Logic (PPTL). Further, examples are given to show how properties of open systems can be specified by APTL formulas. Moreover, to establish the automata based model theory for the new proposed logic, Generalized alternating Büchi automata over Concurrent Game structures (GBCGs) are defined, and a transformation from APTL formulas to GBCGs is presented. In addition, a decision procedure for checking the satisfiability of APTL formulas, and a model checking approach for APTL with Concurrent Game Structures (CGSs) being models are presented.

TCS Journal 2018 Journal Article

A compiler for MSVL and its applications

Kai Yang
Zhenhua Duan
Cong Tian
Nan Zhang

In this paper, we present a method for implementing a compiler called MC for Modeling, Simulation and Verification Language (MSVL) based on LLVM. MC accepts a well formed MSVL program as input and generates an executable binary code. Different from other compilers, MC can be used not only to compile programs but also to model and verify programs. The details of implementation including the architecture design, lexical, syntactic and semantic analysis, as well as preprocessing and scheduling algorithms. Besides, we show MC can be utilized as an infrastructure for Artificial Intelligence (AI) planning. Several examples are given to show applications of MC in modeling and verifying programs, as well as AI planning.

IJCAI Conference 2017 Conference Paper

Temporalising Separation Logic for Planning with Search Control Knowledge

Xu Lu
Cong Tian
Zhenhua Duan

Temporal logics are widely adopted in Artificial Intelligence (AI) planning for specifying Search Control Knowledge (SCK). However, traditional temporal logics are limited in expressive power since they are unable to express spatial constraints which are as important as temporal ones in many planning domains. To this end, we propose a two-dimensional (spatial and temporal) logic namely PPTL^SL by temporalising separation logic with Propositional Projection Temporal Logic (PPTL). The new logic is well-suited for specifying SCK containing both spatial and temporal constraints which are useful in AI planning. We show that PPTL^SL is decidable and present a decision procedure. With this basis, a planner namely S-TSolver for computing plans based on the spatio-temporal SCK expressed in PPTL^SL formulas is developed. Evaluation on some selected benchmark domains shows the effectiveness of S-TSolver.

TCS Journal 2016 Journal Article

A canonical form based decision procedure and model checking approach for propositional projection temporal logic

Zhenhua Duan
Cong Tian
Nan Zhang

This paper proposes a Canonical Form (CF) for chop formulas of Propositional Projection Temporal Logic (PPTL). Based on CF, an improved algorithm for constructing Labeled Normal Form Graph (LNFG) of a PPTL formula is presented. This improvement leads to a better decision procedure for PPTL with infinite models. In addition, a transformation from LNFGs to Generalized Büchi Automata (GBA) and then Büchi Automata (BA) is formalized. Thus, a SPIN based model checking approach is generalized for PPTL. To illustrate how these algorithms work, several examples are given.

TCS Journal 2016 Journal Article

A complete axiom system for propositional projection temporal logic with cylinder computation model

Nan Zhang
Zhenhua Duan
Cong Tian

To specify and verify multi-core parallel programs in a uniform framework, this paper proposes an axiom system for CCM–PPTL which extends that of PPTL by including transformation rules for sequence expressions and axioms as well as inference rules on the CCM construct. Further, the soundness and completeness of the extended axiom system are proved.

IJCAI Conference 2016 Conference Paper

A Decision Procedure for a Fragment of Linear Time Mu-Calculus

Yao Liu
Zhenhua Duan
Cong Tian

In this paper, we study an expressive fragment, namely Gmu, of linear time mu-calculus as a high-level goal specification language. We define Goal Progression Form (GPF) for Gmu formulas and show that every closed formula can be transformed into this form. Based on GPF, we present the notion of Goal Progression Form Graph (GPG) which can be used to describe models of a formula. Further, we propose a simple and intuitive GPG-based decision procedure for checking satisfiability of Gmu formulas which has the same time complexity as the decision problem of Linear Temporal Logic (LTL). However, Gmu is able to express a wider variety of temporal goals compared with LTL.

TCS Journal 2016 Journal Article

A mechanism of function calls in MSVL

Nan Zhang
Zhenhua Duan
Cong Tian

Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it more practical and easier to use, we extend MSVL with external and internal function calls. To do so, the syntax of function definitions and function calls is formalized. Then, the syntax of expressions in MSVL is extended by including function calls. Further, the evaluation rules are redefined. Moreover, the set of statements in MSVL is also extended and the semantics of function call statements is formalized. In addition, the existence of minimal models of MSVL programs involving new added statements is proved. Finally, an example is given to illustrate how to interpret function calls in practice with MSVL.

TCS Journal 2015 Journal Article

Improved even order magic square construction algorithms and their applications in multi-user shared electronic accounts

Zhenhua Duan
Jin Liu
Jie Li
Cong Tian

This paper presents improved even order magic square construction algorithms, including both single even order magic square and double even order magic square construction algorithms. Further, in order to show how the algorithms work, two specific magic squares are constructed. Moreover, the correctness of the algorithms is proved, and the complexity analysis of the algorithms is given. Finally, the improved even order magic square construction algorithms are applied in secure communication and authentication areas for multi-user shared electronic account in detail.

TCS Journal 2014 Journal Article

A formal proof of the deadline driven scheduler in PPTL axiomatic system

Nan Zhang
Zhenhua Duan
Cong Tian
Dingzhu Du

This paper presents an approach for verifying the correctness of the feasibility theorem on the deadline driven scheduler (DDS) with the axiom system of Propositional Projection Temporal Logic (PPTL). To do so, the deadline driven scheduling algorithm is modeled by an MSVL (Modeling, Simulation and Verification Language) program and the feasibility theorem is formulated by PPTL formulas with two parts: a necessary part and a sufficient part. Then, several lemmas are abstracted and proved by means of the axiom system of PPTL. With the help of the lemmas, two parts of the theorem are deduced respectively. This case study convinces us that some real-time properties of systems can be formally verified by theorem proving using the axiom system of PPTL.

TCS Journal 2014 Journal Article

A practical decision procedure for Propositional Projection Temporal Logic with infinite models

Zhenhua Duan
Cong Tian

This paper presents a practical decision procedure for Propositional Projection Temporal Logic with infinite models. First, a set Prop l of labels l i, 0 ⩽ i ⩽ n ∈ N 0, is used to mark nodes of an LNFG of a formula, and a node with l i is treated as an accepting state as in an automaton. Further, the generalized Büchi accepting condition for automata is employed to identify a path (resulting a word) in an LNFG as a model of the formula. In addition, the implementation details of the decision procedure and relevant algorithms including pre-processing, LNFG, circle finding algorithms are presented; as a matter of fact, all algorithms are implemented by C++ programs.

TCS Journal 2013 Journal Article

A complete proof system for propositional projection temporal logic

Zhenhua Duan
Nan Zhang
Maciej Koutny

The paper presents a proof system for Propositional Projection Temporal Logic (PPTL) with projection-plus. The syntax, semantics, and logical laws of PPTL are introduced together with an axiom system consisting of axioms and inference rules. To facilitate proofs, some of the frequently used theorems are proved. A normal form of PPTL formulas is presented, and the soundness and completeness of the proof system are demonstrated. To show how the axiom system works, a full omega regular property for the mutual exclusion problem is specified by a PPTL formula and then a deductive proof of the property is performed.

TCS Journal 2013 Journal Article

A cylinder computation model for many-core parallel computing

Nan Zhang
Zhenhua Duan
Cong Tian

Many-core parallel computing and programming are new challenges to formal specification and verification. This paper presents a semantic model for many-core parallel computing systems so that the systems can be modeled and verified in a manageable way. The model is called Cylinder Computation Model (CCM) which is based on projection constructs in Projection Temporal Logic (PTL) and Modeling, Simulation and Verification Language (MSVL). To this end, the syntax and semantics of CCM are presented in detail. Further, some logic laws regarding CCM are given and the normal form of CCM programs is formalized and proved. Moreover, the operational semantics of CCM and an algorithm for implementing CCM programs within MSVL are also demonstrated. Finally, an example, simple word processor, is given to show how CCM works under MSVL paradigm.

TCS Journal 2012 Journal Article

An efficient approach for abstraction-refinement in model checking

Cong Tian
Zhenhua Duan
Nan Zhang

Abstraction is one of the most important strategies for dealing with the state space explosion problem in model checking. In an abstract model, the state space is largely reduced, however, a counterexample found in such a model may not be a real counterexample. Accordingly, the abstract model needs to be further refined where an NP-hard state separation problem is often involved. In this paper, a novel approach is presented, in which extra boolean variables are added to the abstract model for the refinement. With this approach, not only the NP-hard state separation problem can be avoided, but also a smaller refined abstract model can be obtained.

TCS Journal 2011 Journal Article

Expressiveness of propositional projection temporal logic with star

Cong Tian
Zhenhua Duan

This paper investigates the expressiveness of Propositional Projection Temporal Logic with Star (PPTL*). To this end, Büchi automata and ω -regular expressions are first extended as Stutter Büchi Automata (SBA) and Extended Regular Expressions (ERE) to include both finite and infinite strings. Further, by equivalent transformations among PPTL* formulas, SBAs and EREs, PPTL* is proved to represent exactly the full regular language. Moreover, some fragments of PPTL* are characterized, and finally, PPTL* and its fragments are classified into five different language classes.

LPAR Conference 1994 Conference Paper

Projection in Temporal Logic Programming

Zhenhua Duan
Maciej Koutny
Chris Holt

Abstract We define a projection operator in the framework of the temporal logic programming. Its syntax and semantics are presented and illustrated with examples. We also discuss the implementation details of the projection construct.