Chanjuan Liu 0001

dblp:39/7714-1 · also Chan-Juan Liu 0001 · DBLP profile ↗
← Back
35ranked-venue papers
12as first author
28since 2021 · last 2026
—ORCID · conflict

Domains — the database's venue-derived domains; a paper can count in several

Artificial intelligence and machine learning · 16 · 6 first-author · 14 since 2021Databases, data management, data science and information retrieval · 8 · 3 first-author · 7 since 2021Theory of computation · 5 · 3 first-author · 1 since 2021Applied, interdisciplinary, general and emerging computing · 4 · 1 first-author · 3 since 2021Systems, architecture and hardware · 1 · 1 since 2021Computer networks · 1 · 1 since 2021Software engineering, systems software and programming languages · 1 · 1 since 2021Graphics, computer vision, multimedia, augmented reality and games · 1 · 1 since 2021Human-computer interaction and ubiquitous computing · 1 · 1 since 2021
YearPublicationVenuePosition
2026 Exact Optimization for Minimum Dominating Sets
abstract
The Minimum Dominating Set (MDS) problem is a well-established combinatorial optimization problem with numerous real-world applications. Its NP-hard nature makes it increasingly difficult to obtain exact solutions as the graph size grows. This paper introduces ParDS, an exact algorithm developed to address the MDS problem within the branch-and-bound framework. ParDS features two key innovations: an advanced linear programming technique that yields tighter lower bounds and a set of novel reduction rules that dynamically simplify instances throughout the solving process. Compared to the leading exact algorithms presented at IJCAI 2023 and 2024, ParDS demonstrates theoretically superior lower-bound quality. Experimental results on standard benchmark datasets highlight several significant advantages of ParDS: it achieves fastest solving times in 70% of graph categories, especially on large, sparse graphs, delivers a speed-up of up to 3,411 times on the fastest individual instance, and successfully solves 16 out of 43 instances that other algorithms were unable to resolve within the 5-hour time limit. These findings establish ParDS as a state-of-the-art solution for exactly solving the MDS problem
Enqiang Zhu, Yu Zhang 0231, Chanjuan Liu 0001, Pu Wu
AAAI4
2026 Mining Large Independent Sets on Massive Graphs
Yu Zhang 0231, Witold Pedrycz, Chanjuan Liu 0001, Enqiang Zhu
DASFAA (5)3
2026 Cohesive Group Discovery in Interaction Graphs under Explicit Density Constraints
abstract
Discovering cohesive groups is a fundamental primitive in graph-based recommender systems, underpinning tasks such as social recommendation, bundle discovery, and community-aware modeling. In interaction graphs, cohesion is often modeled as the γ-quasi-clique, an induced subgraph whose internal edge density meets a user-defined threshold γ. This formulation provides explicit control over within-group connectivity while accommodating the sparsity inherent in real-world data. However, ensuring explicit density constraints while maintaining robustness remains challenging for existing heuristic approaches. This paper presents EDQC, an effective framework for cohesive group discovery under explicit density constraints. EDQC leverages a lightweight energy diffusion process to rank vertices for localizing promising candidate regions. Guided by this ranking, the framework extracts and refines a candidate subgraph to ensure the output strictly satisfies the target density requirement. Extensive experiments on 75 real-world graphs across varying density thresholds demonstrate that EDQC identifies the largest mean γ-quasi-cliques in the vast majority of cases, achieving lower variance than the state-of-the-art methods while maintaining competitive runtime, making it a robust and practical solution for cohesive group discovery in graph-based recommender systems.
Yu Zhang 0231, Yilong Luo, Mingyuan Ma, Enqiang Zhu, Jin Xu 0002, Chanjuan Liu 0001
SIGIR7
2026 Heuristic-based dynamic graph actor-critic algorithm for information path planning
Ruining Zhang, Chanjuan Liu 0001, Hong-Wei Ge
Expert Syst. Appl.2
2026 Multi-view clustering via diversity consensus graph infusion
Mingguang Shao, Jian Wang 0010, Chanjuan Liu 0001, Peiying Zhang 0001, Nikhil R. Pal
Neurocomputing3
2026 RHMGSA: Reinforcement learning-guided evolutionary search for critical node detection
Xiancheng Feng, Jingkun Fan, Chanjuan Liu 0001, Enqiang Zhu, Witold Pedrycz
Inf. Sci.3
2026 Dynamic location search for identifying maximum weighted independent sets in complex networks
Enqiang Zhu, Chenkai Hao, Chanjuan Liu 0001, Yongsheng Rao
Inf. Sci.4
2026 CirOPT: Toward Effective Combinational Equivalence Checking via Compiler Optimization
abstract
Combinational equivalence checking (CEC) is essential for verifying the correctness of circuit designs. With the growing complexity of circuits, effective verification techniques have become increasingly critical. Recently, a conjunctive normal form (CNF)-based approach, converting circuits to CNF for Boolean satisfiability (SAT) solvers, has shown competitive performance compared to state-of-the-art hybrid SAT sweeping approaches. The capability of this CNF-based approach depends on effective CNF conversion. This work presentsCirOPT, which is the first CNF conversion method using compiler optimization to equivalently simplify circuits. Extensive experiments are conducted on a broad range of real-world benchmarks, which are far more than the number of benchmarks typically used in empirical studies. The results reveal that, when paired with the state-of-the-art CNF SAT solverKissat,CirOPTconsiderably outperforms existing approaches in CEC.
Shaoke Cui, Chuan Luo 0002, Zhenwei Yang, Jiabao Lin, Wei Wu 0011, Chanjuan Liu 0001, Shaowei Cai 0001, Chunming Hu
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.6
2026 Guiding Multiagent Multitask Reinforcement Learning by a Hierarchical Framework With Logical Reward Shaping
abstract
Multiagent hierarchical reinforcement learning (MAHRL) has been studied as an effective means to solve intelligent decision problems in complex and large-scale environments. However, most current MAHRL algorithms follow the traditional way of using reward functions in reinforcement learning (RL), which limits their use to a single task. This study aims to design a multiagent cooperative algorithm with logic reward shaping (LRS), which uses a more flexible way of setting the rewards, allowing for the effective completion of multitasks. LRS uses linear-time temporal logic (LTL) to express the internal logic relation of subtasks within a complex task. Then, it evaluates whether the subformulas of the LTL expressions are satisfied based on a designed reward structure. This helps agents to learn to effectively complete tasks by adhering to the LTL expressions, thus enhancing the interpretability and credibility of their decisions. To enhance coordination and cooperation among multiple agents, a value iteration technique is designed to evaluate the actions taken by each agent. Based on this evaluation, a reward function is shaped for coordination, which enables each agent to evaluate its status and complete the remaining subtasks through experiential learning. Experiments have been conducted on various types of tasks in the Minecraft World and Office World. The results demonstrate that the proposed algorithm can improve the performance of multiagents when learning to complete multitasks.
Chanjuan Liu 0001, Jinmiao Cong, Bingcai Chen, Yaochu Jin, Enqiang Zhu
IEEE Trans. Cybern.1
2026 HyColor: An Efficient Heuristic Algorithm for Graph Coloring
abstract
The graph coloring problem (GCP) is a classic combinatorial optimization problem that aims to find the minimum number of colors assigned to the vertices of a graph such that no two adjacent vertices receive the same color. GCP has been extensively studied by researchers from various fields, including mathematics, computer science, and biological science. Due to the$\mathcal {NP}$-hard nature, many heuristic algorithms have been proposed to solve GCP. However, existing GCP algorithms focus on either small hard graphs or large-scale sparse graphs (with up to$10^{7}$vertices). This article presents an efficient hybrid heuristic algorithm for GCP, namedHyColor, which excels in handling large-scale sparse graphs while achieving impressive results on small dense graphs. The efficiency ofHyColorcomes from the following three aspects: 1) a local decision strategy to improve the lower bound on the chromatic number; 2) a graph-reduction strategy to reduce the working graph; and 3) a$k$-core and mixed degree-based greedy heuristic for efficiently coloring graphs.HyColoris evaluated against three state-of-the-art GCP algorithms across four benchmarks, comprising three large-scale sparse graph benchmarks and one small dense graph benchmark, totaling 209 instances. The results demonstrate thatHyColorconsistently outperforms existing heuristic algorithms in both solution accuracy and computational efficiency for the majority of instances. Notably,HyColorachieved the best solutions in 194 instances (over 93%), with 34 of these solutions significantly surpassing those of other algorithms. Furthermore,HyColorsuccessfully determined the chromatic number and achieved optimal coloring in 128 instances.
Enqiang Zhu, Yu Zhang 0231, Haopeng Sun, Ziqi Wei 0001, Witold Pedrycz, Chanjuan Liu 0001, Jin Xu 0002
IEEE Trans. Syst. Man Cybern. Syst.6
2025 SMTgazer: Learning to Schedule SMT Algorithms via Bayesian Optimization
abstract
Satisfiability Modulo Theories (SMT) plays a critical role in various software engineering applications, including program verification, symbolic execution, and automated test generation. Over the years, a wide range of SMT solvers has been developed, typically designed for general purposes or tailored to specific background theories, such as bit-vectors or nonlinear arithmetic. Due to the diversity and complexity of SMT instances, no single solver consistently outperforms others across all problem domains. This motivates the need for algorithm selection strategies that can adaptively choose solvers based on the characteristics of the instances.To overcome the limitations of single-solver selection, solving SMT as a scheduling problem, enabling a more fault-tolerant and effective use of multiple solvers in sequence. We model algorithm scheduling as a hyperparameter optimization problem, enabling efficient black-box search over solver sequences while treating the dataset as a whole, thus achieving globally optimized and robust scheduling strategies. The resulting scheduler called SMTgazer. To further enhance scheduling efficiency and solver performance, we propose two optimizations: leveraging unsupervised X-means clustering to create semantically coherent instance groups for localized model training, and augmenting the Bayesian optimization surrogate with boosting and bagging ensembles to improve generalization and mitigate overfitting, thereby yielding more reliable performance predictions for the sequential portfolio scheduler.Extensive experiments are conducted to evaluate the performance of SMTgazer, utilizing six SMT benchmarks derived from real-world applications. It shows that our approach consistently outperforms current state-of-the-art methods. Particularly, SMTgazer achieves a 44.65% reduction in PAR-2 score and 69.11% decrease in the number of unsolved instances, compared to the strongest competitor, Sibyl, demonstrating the effectiveness of formulating SMT algorithm scheduling as a hyperparameter optimization problem. We further analyze the generated scheduling sequences to uncover the design principles that explain the success of our method. Finally, we also empirically show that our approach is both robust and generalizable, and the proposed strategies are effective.
Chuan Luo 0002, Shaoke Cui, Jianping Song, Xindi Zhang 0001, Wei Wu 0011, Chanjuan Liu 0001, Shaowei Cai 0001, Chunming Hu
ASE6
2025 Optimizing local search-based partial MaxSAT solving via initial assignment prediction
Chanjuan Liu 0001, Chuan Luo 0002, Shaowei Cai 0001, Zhendong Lei, Wenjie Zhang 0007, Yi Chu, Guojing Zhang
Sci. China Inf. Sci.1
2025 Critical nodes detection for complex networks via knowledge-guided evolutionary framework
Chanjuan Liu 0001, Shike Ge, Zhihan Chen 0001, Wenbin Pei, Enqiang Zhu, Hisao Ishibuchi
Eng. Appl. Artif. Intell.1
2025 Adaptive Tokenization Transformer: Enhancing Irregularly Sampled Multivariate Time-Series Analysis
abstract
Analyzing irregularly sampled multivariate time series (ISMTS) data poses significant challenges, with such irregularities frequently occurring in contexts like the Industrial Internet of Things (IIoT). However, most existing methods are designed for regularly sampled data, limiting their effectiveness in handling such complexities. These traditional approaches struggle with misalignments across time and variate dimensions, often requiring extensive preprocessing that can result in information loss and the introduction of noise. Furthermore, they may incorrectly utilize processing units, such as variate or temporal tokens, leading to suboptimal performance. To tackle these challenges, we present the Adaptive Tokenization Transformer (ATFormer), an innovative model designed to improve the analysis of ISMTS data. ATFormer employs an adaptive mechanism to select appropriate tokens (temporal or variate) based on the unique characteristics of the time series data. By capturing each observation at a finer granularity, the model enhances token representation. A masked attention mechanism aggregates observations, creating more comprehensive tokens and embedding information consistently, thereby mitigating incomplete embeddings and noise. Additionally, ATFormer facilitates the formation of fine-grained tokens and performs coarse-grained self-attention operations, enhancing the model’s utilization of tokens through the interaction of information at different granularities. This multilevel processing allows the model to effectively capture detailed information while integrating broader features, ultimately improving overall performance. Our evaluations on two healthcare datasets and one human activity dataset demonstrate that ATFormer outperforms existing methods in analyzing ISMTS.
Enqiang Zhu, Chanjuan Liu 0001, Jian Wang 0010
IEEE Internet Things J.3
2025 A new EGO-driven memetic algorithm for solving flexible job shop scheduling problem
Chanjuan Liu 0001, Guojing Zhang, Bingcai Chen, Hisao Ishibuchi
Inf. Sci.1
2025 A DNA Strand Displacement-Based Computing Model for Solving Intractable Graph Problems
abstract
Graphs are the primary means of describing the relation between individuals in society, and have been extensively used for analysing various types of networks, such as social networks, biological networks, and electric networks. Many practical problems can be abstracted to graph problems, and cannot be solved efficiently due to their NP-hard nature. DNA computing, leveraging the vast parallelism and high-density storage of DNA molecules, provides a new way for solving intractable problems. However, existing DNA computing models are limited by single computing function. This paper proposed a novel DNA computing model with two DNA modules-a graph representation module (GRM) and a detection module (DM)-that can solve a variety of NP-hard problems. To show the feasibility of the proposed model, we conducted simulation and biochemical experiments on multiple NP-hard problems, such as the minimum dominating set, maximum independent set, and minimum vertex cover. Experimental results showed that the GRM is a universal graph representation module, based on which multiple graph problems can be solved by cascading a proper designed detection module. Our method also highlighted the potential for DNA strand displacement to act as a computation tool to solve intractable graph problems.
Enqiang Zhu, Xianhang Luo, Chanjuan Liu 0001, Jin Xu 0002
IEEE Trans. Comput. Biol. Bioinform.3
2025 Constructing Concise Instance-Based Takagi-Sugeno-Kang Fuzzy Systems via Multiobjective Particle Swarm Optimization
abstract
Takagi-Sugeno-Kang (TSK) fuzzy system has been successfully applied to various practical problems due to its good performance and interpretability. One important prerequisite for the interpretability of a fuzzy system is a concise rule base. However, how to construct a concise TSK fuzzy system more transparently and adaptively from data remains a challenge. In this article, we propose a two-phase framework of constructing concise instance-based TSK fuzzy systems using a novel multi objective particle swarm optimization algorithm with a bimutation strategy (MOPSO-BM). In the first phase, a basic fuzzy system is constructed, where the rule antecedents are initialized based on some representative input instances selected by a sample filtering algorithm, and the consequent parameters are obtained by least squares estimation. Then in the second phase, the proposed MOPSO-BM algorithm is utilized to further reduce the number of fuzzy rules and fine-tune the consequent parameters, resulting in a set of fuzzy systems that achieve a good trade-off between accuracy and interpretability. Users have the flexibility to select the most suitable model based on their specific requirements, or simply via cross validation. Numerical experiments on twelve benchmark datasets have substantiated the superior performance of the proposed framework in designing high-precision and compact TSK fuzzy systems.
Qin Chang, Chanjuan Liu 0001, Jian Wang 0010
IEEE Trans. Fuzzy Syst.4
2025 Boosting Reinforcement Learning via Hierarchical Game Playing With State Relay
abstract
Due to its wide application, deep reinforcement learning (DRL) has been extensively studied in the motion planning community in recent years. However, in the current DRL research, regardless of task completion, the state information of the agent will be reset afterward. This leads to a low sample utilization rate and hinders further explorations of the environment. Moreover, in the initial training stage, the agent has a weak learning ability in general, which affects the training efficiency in complex tasks. In this study, a new hierarchical reinforcement learning (HRL) framework dubbed hierarchical learning based on game playing with state relay (HGR) is proposed. In particular, we introduce an auxiliary penalty to regulate task difficulty, and one training mechanism, the state relay mechanism, is designed. The relay mechanism can make full use of the intermediate states of the agent and expand the environment exploration of low-level policy. Our algorithm can improve the sample utilization rate, reduce the sparse reward problem, and thereby enhance the training performance in complex environments. Simulation tests are carried out on two public experiment platforms, i.e., MazeBase and MuJoCo, to verify the effectiveness of the proposed method. The results show that HGR significantly benefits the reinforcement learning (RL) area.
Chanjuan Liu 0001, Jinmiao Cong, Guifei Jiang, Xirong Xu, Enqiang Zhu
IEEE Trans. Neural Networks Learn. Syst.1
2024 SlideMLP: A Pure Multi-layer Perceptrons Method For Medical Image Segmentation
abstract
Convolutional Neural Networks and Attention-based Transformer have emerged as the preferred models for medical image processing. Recently, specific network architectures relying solely on multilayer perceptrons (MLPs) have gained popularity and demonstrated excellent results in various computer vision tasks. In particular, CycleMLP has demonstrated good performance in dense prediction tasks owing to its adaptability to image size and linear computational complexity. However, the basic operator of CycleMLP has a fixed sampling location for any feature map and samples very few target organs in medical images characterized by an extreme imbalance between foreground and background. Therefore, effectively extracting the features of target organs becomes challenging. In this paper, we propose a new MLP-like module, SlideMLP, by considering the sparsity of target organs in medical images. This module extracts a set of offsets from the input feature maps and utilizes these offsets to re-select the sampling points. This approach effectively enhances the sampling rate of target organs while retaining the advantages of CycleMLP. Additionally, we constructed a U-shaped network with a pure MLP using this module and assessed its robustness using two datasets with different modalities. Comparative results with state-of-the-art methods demonstrate that the method proposed in this paper can achieve a substantial Dice Similarity Coe cient (DSC) while utilizing fewer parameters.
Chaoqi Han, Bingcai Chen, Chanjuan Liu 0001, Qian Ning, Victor C. M. Leung, Shouzhen Jiao
IJCNN3
2024 SDI: A tool for speech differentiation in user identification
Muhammad Abdul Basit, Chanjuan Liu 0001, Enyu Zhao
Expert Syst. Appl.2
2024 PHEE: Identifying influential nodes in social networks with a phased evaluation-enhanced search
Enqiang Zhu, Yu Zhang 0231, Chanjuan Liu 0001
Neurocomputing5
2024 Heuristic Search with Cut Point Based Strategy for Critical Node Problem
Zhihan Chen 0001, Shaowei Cai 0001, Jian Gao 0007, Shike Ge, Chanjuan Liu 0001, Jinkun Lin
J. Comput. Sci. Technol.5
2024 A dual-mode local search algorithm for solving the minimum dominating set problem
Enqiang Zhu, Yu Zhang 0231, Darren Strash, Chanjuan Liu 0001
Knowl. Based Syst.5
2023 A Heuristic Framework for Personalized Route Recommendation Based on Convolutional Neural Networks
Ruining Zhang, Chanjuan Liu 0001, Qiang Zhang 0008, Xiaopeng Wei
PRICAI (3)2
2023 Identifying the cardinality-constrained critical nodes with a hybrid evolutionary algorithm
Chanjuan Liu 0001, Shike Ge, Yuanke Zhang
Inf. Sci.1
2022 Partition Independent Set and Reduction-Based Approach for Partition Coloring Problem
abstract
Given a graph whose vertex set is partitioned, the partition coloring problem (PCP) requires the selection of one vertex from each partite set, such that the subgraph induced by the set of the selected vertices has the minimum chromatic number. Motivated by the routing and wavelength assignment problem for optical networks, PCP has been used to model many other real-world applications, such as dichotomy-based constraint encoding and scheduling problems. Solving PCP for large graphs is still a challenge since it is NP -complete. In this article, we first propose a key concept called a partition independent set (PIS) and design an efficient algorithm called FastPIS to find a maximum PIS. By applying FastPIS with a simple coloring procedure, we can obtain a high-quality initial solution for PCP. Moreover, we propose a reduction rule based on another novel concept called an l -clustering-degree bound ordered set ( l -CDBOS), by which the scale of the working graph can be iteratively reduced. Based on these techniques, we develop an efficient method called HotPGC for solving PCP. The proposed algorithm is evaluated on benchmark graphs, and computational results show that HotPGC achieves highly competitive performance, compared with the state-of-the-art algorithms. The influence of the proposed reduction rule on the efficiency of HotPGC is also analyzed.
Enqiang Zhu, Chanjuan Liu 0001, Jin Xu 0002
IEEE Trans. Cybern.3
2021 A note on domination number in maximal outerplanar graphs
Chanjuan Liu 0001
Discret. Appl. Math.1
2021 Exploring the effects of computational costs in extensive games via modeling and simulation
abstract
Game theory has become a standard tool for depicting and demonstrating various game-like phenomena by providing appropriate mathematical models and for analyzing and predicting agents' behaviors and their decisions by formalizing solution concepts. The conventional game model mainly concerns ideal systems that would always guarantee optimal responses, which appears unrealistic for practical game scenarios since decision-making usually entails resource costs. Therefore, this study considers players' decision-making in extensive games when the computational cost of searching the strategy space is limited. We start with a new mathematical model of extensive games that features a bound on computational resources during players' decision-making process such that they can only foresee a part of the available alternatives in the future. This model is more appropriate in predicting players' strategies than the conventional model, under which we investigate the effects of computational costs on players' strategies as well as the computational complexity. Furthermore, a simulation experiment is performed to seek the connection between the amount of resources and the goodness of the outcomes. This study is expected to provide a foundation for players' rational decision-making with computational costs.
Chanjuan Liu 0001, Enqiang Zhu, Qiang Zhang 0008, Xiaopeng Wei
Int. J. Intell. Syst.1
2019 On the semitotal domination number of line graphs
Enqiang Zhu, Chanjuan Liu 0001
Discret. Appl. Math.2
2018 A Dynamic-Logical Characterization of Solutions to Sight-limited Extensive Games
abstract
An unrealistic assumption in classical extensive game theory is that the complete game tree is fully perceivable by all players. To weaken this assumption, a class of games (called games with short sight) was proposed in literature, modelling the game scenarios where players have only limited fores ight of the game tree due to bounded resources and limited computational ability. As a consequence, the notions of equilibria in classical game theory were refined to fit games with short sight. A crucial issue that thus arises is to determine whether a strategy profile is a solution to a game. To study this issue and address the underlying idea and theory on players’ decisions in such games, we adopt a logical way. Specifically, we develop a logic called DLS through which features of these games are demonstrated. More importantly, it enables us to characterize the solutions to these games via formulas of this logic. Moreover, we study the algorithm for model checking DLS, which is shown to be PTIME-complete in the size of the model. This work not only provides an insight into a more realistic model in game theory, but also enriches the possible applications of logic.
Chanjuan Liu 0001, Fenrong Liu, Kaile Su
Fundam. Informaticae1
2018 Modeling of Agent Cognition in Extensive Games via Artificial Neural Networks
abstract
The decision-making process, which is regarded as cognitive and ubiquitous, has been exploited in diverse fields, such as psychology, economics, and artificial intelligence. This paper considers the problem of modeling agent cognition in a class of game-theoretic decision-making scenarios called extensive games. We present a novel framework in which artificial neural networks are incorporated to simulate agent cognition regarding the structure of the underlying game and the goodness of the game situations therein. An algorithmic procedure is investigated to describe the process for solving games with cognition, and then, a new equilibrium concept is proposed as a refinement of the classical one-subgame perfect equilibrium-by involving players' cognitive reasoning. Moreover, a series of results concerning the computational complexity, soundness, and completeness of the algorithm, as well as the existence of an equilibrium solution, is obtained. This framework, which is shown to be general enough to model the way in which AlphaGo plays Go, may offer a means for bridging the gap between theoretical models and practical problem-solving.
Chanjuan Liu 0001, Enqiang Zhu, Qiang Zhang 0008, Xiaopeng Wei
IEEE Trans. Neural Networks Learn. Syst.1
2016 A logical characterization of extensive games with short sight
Chanjuan Liu 0001, Fenrong Liu, Kaile Su, Enqiang Zhu
Theor. Comput. Sci.1
2015 A Dynamic-Logical Characterization of Solutions in Sight-Limited Extensive Games
Chanjuan Liu 0001, Fenrong Liu, Kaile Su
PRIMA1
2015 Tree-core and tree-coritivity of graphs
Enqiang Zhu, Zepeng Li 0003, Zehui Shao, Jin Xu 0002, Chanjuan Liu 0001
Inf. Process. Lett.5
2010 Automatic Verification of Web Service Protocols for Epistemic Specifications under Dolev-Yao Model
abstract
Web service protocols are designed in XML formats so the message structures within are quite different from the conventional protocols. Therefore, the traditional formal verification techniques which have gain substantial achievements in practice, cannot be applied directly to them because their underlying models are written in Alice\Bob-style descriptions using high-level message formats instead of XML tags. In this paper, we propose a justification-oriented and automatic formal approach to verify, in the standard Dolev-Yao model, security properties expressed as epistemic notions for a Web service protocol, based on a fault-preserving mapping tool called SuD (SOAP under Dolev-Yao). Our approach can shed more light on Web service protocols in another perspective because the concerned properties to be verified are some inherent features of protocols.
Qingliang Chen, Kaile Su, Chanjuan Liu 0001, Yinyin Xiao
ICSS3