检索结果-内蒙古大学图书馆

MODEL CHECKING FOR MULTI-AGENT SYSTEMS MODELED BY EPISTEMIC PROCESS CALCULUS

学校读者我要写书评

暂无评论

arXiv 2025年

作者： Yu, Qixian Cao, Zining Hui, Zong Zhou, Yuan College of Computer Science and Technology Nanjing University of Aeronautics and Astronautics Nanjing211106 China Ministry Key Laboratory for Safety-Critical Software Development and Verification Nanjing211106 China Collaborative Innovation Center of Novel Software Technology and Industrialization Nanjing210023 China Faculty of Computer and Software Engineering Huaiyin Institute Of Technology Huaian223001 China

This paper presents a comprehensive framework for modeling and verifying multi-agent systems. The paper introduce an Epistemic Process Calculus for multi-agent systems, which formalizes the syntax and semantics to capture the essential features of agent behavior interactions and epistemic states. Building upon this calculus, we propose ATLE, an extension of Alternating-time Temporal Logic incorporating epistemic operators to express complex properties related to agent epistemic state. To verify ATLE specifications, this paper presents a model checking algorithm that systematically explores the state space of a multi-agent system and evaluates the satisfaction of the specified properties. Finally, a case study is given to demonstrate the method. © 2025, CC BY.

关键词： Multi agent systems

A Simple Geometric-Aware Indoor Positioning Interpolation Algorithm Based on Manifold Learning

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Yang, Suorong Zhang, Geng Zhao, Jian Shen, Furao State Key Laboratory for Novel Software Technology Nanjing University China Department of Computer Science and Technology Nanjing University China School of Artificial Intelligence Nanjing University China School of Electronic Science and Engineering Nanjing University China

Interpolation methodologies have been widely used within the domain of indoor positioning systems. However, existing indoor positioning interpolation algorithms exhibit several inherent limitations, including reliance on complex mathematical models, limited flexibility, and relatively low precision. To enhance the accuracy and efficiency of indoor positioning interpolation techniques, this paper proposes a simple yet powerful geometric-aware interpolation algorithm for indoor positioning tasks. The key to our algorithm is to exploit the geometric attributes of the local topological manifold using manifold learning principles. Therefore, instead of constructing complicated mathematical models, the proposed algorithm facilitates the more precise and efficient estimation of points grounded in the local topological manifold. Moreover, our proposed method can be effortlessly integrated into any indoor positioning system, thereby bolstering its adaptability. Through a systematic array of experiments and comprehensive performance analyses conducted on both simulated and real-world datasets, we demonstrate that the proposed algorithm consistently outperforms the most commonly used and representative interpolation approaches regarding interpolation accuracy and efficiency. Furthermore, the experimental results also underscore the substantial practical utility of our method and its potential applicability in real-time indoor positioning scenarios. Copyright © 2023, The Authors. All rights reserved.

关键词： Interpolation

IAACS: Image aesthetic assessment through color composition and space formation

学校读者我要写书评

暂无评论

Virtual Reality & Intelligent Hardware 2023年第1期5卷 42-56页

作者： Bailin YANG Changrui ZHU Frederick WBLI Tianxiang WEI Xiaohui LIANG Qingxu WANG School of Computer and Information Engineering Zhejiang Gongshang UniversityHangzhou 310018China Department of Computer Science University of DurhamDH13LEUnited Kingdom College of Intelligence and Computing Tianjin UniversityTianjin 300072China State Key Laboratory of Virtual Reality Technology and Systems Beihang UniversityBeijing 100191China

Background Determining how an image is visually appealing is a complicated and subjective task. This motivates the use of a machine-learning model to evaluate image aesthetics automatically by matching the aesthetics of the general public. Although deep learning methods have successfully learned good visual features from images,correctly assessing the aesthetic quality of an image remains a challenge for deep learning. Methods To address this, we propose a novel multiview convolutional neural network to assess image aesthetics assessment through color composition and space formation(IAACS). Specifically, from different views of an image––including its key color components and their contributions, the image space formation, and the image itself––our network extracts the corresponding features through our proposed feature extraction module(FET) and the Image Net weight-based classification model. Result By fusing the extracted features, our network produces an accurate prediction score distribution for image aesthetics. The experimental results show that we have achieved superior performance.

关键词： Image aesthetic assessment Color composition Space formation Deep learning

The Devil is in the Statistics: Mitigating and Exploiting Statistics Difference for Generalizable Semi-supervised Medical Image Segmentation

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Qiu, Muyang Zhang, Jian Qi, Lei Yu, Qian Shi, Yinghuan Gao, Yang State Key Laboratory for Novel Software Technology Nanjing University China National Institute of Healthcare Data Science Nanjing University China School of Computer Science and Engineering Southeast University School of Data and Computer Science Shandong Women’s University China

Despite the recent success of domain generalization in medical image segmentation, voxel-wise annotation for all source domains remains a huge burden. Semi-supervised domain generalization has been proposed very recently to combat this challenge by leveraging limited labeled data along with abundant unlabeled data collected from multiple medical institutions, depending on precisely harnessing unlabeled data while improving generalization simultaneously. In this work, we observe that domain shifts between medical institutions cause disparate feature statistics, which significantly deteriorates pseudo-label quality due to an unexpected normalization process. Nevertheless, this phenomenon could be exploited to facilitate unseen domain generalization. Therefore, we propose 1) multiple statistics-individual branches to mitigate the impact of domain shifts for reliable pseudo-labels and 2) one statistics-aggregated branch for domain-invariant feature learning. Furthermore, to simulate unseen domains with statistics difference, we approach this from two aspects, i.e., a perturbation with histogram matching at image level and a random batch normalization selection strategy at feature level, producing diverse statistics to expand the training distribution. Evaluation results on three medical image datasets demonstrate the effectiveness of our method compared with recent SOTA methods. The code is available at https://***/qiumuyang/SIAB. © 2024, CC BY.

关键词： Image segmentation

RADAP: A Robust and Adaptive Defense Against Diverse Adversarial Patches on Face Recognition

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Liu, Xiaoliang Shen, Furao Zhao, Jian Nie, Changhai State Key Laboratory for Novel Software Technology Nanjing University China Department of Computer Science and Technology Nanjing University China School of Artificial Intelligence Nanjing University China School of Electronic Science and Engineering Nanjing University China

Face recognition (FR) systems powered by deep learning have become widely used in various applications. However, they are vulnerable to adversarial attacks, especially those based on local adversarial patches that can be physically applied to real-world objects. In this paper, we propose RADAP, a robust and adaptive defense mechanism against diverse adversarial patches in both closed-set and open-set FR systems. RADAP employs innovative techniques, such as FCutout and F-patch, which use Fourier space sampling masks to improve the occlusion robustness of the FR model and the performance of the patch segmenter. Moreover, we introduce an edge-aware binary cross-entropy (EBCE) loss function to enhance the accuracy of patch detection. We also present the split and fill (SAF) strategy, which is designed to counter the vulnerability of the patch segmenter to complete white-box adaptive attacks. We conduct comprehensive experiments to validate the effectiveness of RADAP, which shows significant improvements in defense performance against various adversarial patches, while maintaining clean accuracy higher than that of the undefended Vanilla model. Copyright © 2023, The Authors. All rights reserved.

关键词： Face recognition

A First Step Towards Runtime Analysis of Evolutionary Neural Architecture Search

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Lv, Zeqiong Qian, Chao Sun, Yanan College of Computer Science Sichuan University Chengdu610065 China National Key Laboratory for Novel Software Technology School of Artificial Intelligence Nanjing University Nanjing210023 China

Evolutionary neural architecture search (ENAS) employs evolutionary algorithms to find high-performing neural architectures automatically, and has achieved great success. However, compared to the empirical success, its rigorous theoretical analysis has yet to be touched. This work goes preliminary steps toward the mathematical runtime analysis of ENAS. In particular, we define a binary classification problem UNIFORM, and formulate an explicit fitness function to represent the relationship between neural architecture and classification accuracy. Furthermore, we consider (1+1)-ENAS algorithm with mutation to optimize the neural architecture, and obtain the following runtime bounds: both the local and global mutations find the optimum in an expected runtime of Θ(n), where n is the problem size. The theoretical results show that the local and global mutations achieve nearly the same performance on UNIFORM. Empirical results also verify the equivalence of these two mutation operators. Copyright © 2024, The Authors. All rights reserved.

关键词： Machine learning

Mathematical modeling of mixed convective MHD Falkner-Skan squeezed Sutterby multiphase flow with non-Fourier heat flux theory and porosity

学校读者我要写书评

暂无评论

Applied Mathematics and Mechanics(English Edition) 2023年第11期44卷 2005-2018页

作者： Shuguang LI M.I.KHAN F.ALI S.S.ABDULLAEV S.SAADAOUI HABIBULLAH School of Computer Science and Technology Shandong Technology and Business UniversityYantai 264005Shandong ProvinceChina Department of Mechanics and Engineering Science Peking UniversityBeijing 100871China Department of Mechanical Engineering Lebanese American UniversityBeirut 11020Lebanon Department of Mathematical Sciences Federal Urdu University of ArtsSciences&TechnologyGulshan-e-IqbalKarachi 75300Pakistan Faculty of Chemical Engineering New Uzbekistan UniversityTashkent 100070Uzbekistan Department of Science and Innovation Tashkent State Pedagogical University named after NizamiTashkent 100070Uzbekistan Department of Physics Faculty of Science and ArtsMohayel AserKing Khalid UniversityAbha 61421Saudi Arabia State Key Laboratory of Turbulence and Complex System Collaborative Innovative Center for Advanced Aero-EnginesPeking UniversityBeijing 100871China

In a wide variety of mechanical and industrial applications,e.g.,space cooling,nuclear reactor cooling,medicinal utilizations(magnetic drug targeting),energy generation,and heat conduction in tissues,the heat transfer phenomenon is ***’s law of heat conduction has been used as the foundation for predicting the heat transfer behavior in a variety of real-world *** model’s production of a parabolic energy expression,which means that an initial disturbance would immediately affect the system under investigation,is one of its main ***,numerous researchers worked on such problem to resolve this *** last,this problem was resolved by Cattaneo by adding relaxation time for heat flux in Fourier’s law,which was defined as the time required to establish steady heat conduction once a temperature gradient is *** offered a material invariant version of Cattaneo’s model by taking into account the upper-connected derivative of the Oldroyd ***,both models are combinedly known as the Cattaneo-Christov(CC)*** this attempt,the mixed convective MHD Falkner-Skan Sutterby nanofluid flow is addressed towards a wedge surface in the presence of the variable external magnetic *** CC model is incorporated instead of Fourier’s law for the examination of heat transfer features in the energy expression.A two-phase nanofluid model is utilized for the implementation of *** nonlinear system of equations is tackled through the bvp4c technique in the MATLAB software *** influence of pertinent flow parameters is discussed and displayed through different *** and important results are summarized in the conclusion ***,in both cases of wall-through flow(i.e.,suction and injection effects),the porosity parameters increase the flow speed,and decrease the heat transport and the influence of drag forces.

关键词： sporosity Cattaneo-Christov(CC)heat flux model Falkner-Skan Sutterby nanofluid mixed convection stagnation point

Modular Verification of SPARCv8 Code

学校读者我要写书评

暂无评论

Journal of computer science & technology 2020年第6期35卷 1382-1405页

作者： Jun-Peng Zha Xin-Yu Feng Lei Qiao Department of Computer Science and Technology Nanjing UniversityNanjing 210023China State Key Laboratory for Novel Software Technology Nanjing UniversityNanjing 210023China Beijing Institute of Control Engineering Beijing 100080China

Inline assembly code is common in system software to interact with the underlying hardware platforms. The safety and correctness of the assembly code is crucial to guarantee the safety of the whole system. In this paper, we propose a practical Hoare-style program logic for verifying SPARC (Scalable Processor Architecture) assembly code. The logic supports modular reasoning about the main features of SPARCv8 ISA (instruction set architecture), including delayed control transfers, delayed writes to special registers, and register windows. It also supports relational reasoning for refinement verification. We have applied it to verify that there is a contextual refinement between a context switch routine in SPARCv8 and a switch primitive. The program logic and its soundness proof have been mechanized in Coq.

关键词： Scalable Processor Architecture Version 8(SPARCv8) assembly code verification context switch Coq refinement verification

Visual Style Prompt Learning Using Diffusion Models for Blind Face Restoration

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Lu, Wanglong Wang, Jikai Wang, Tao Zhang, Kaihao Jiang, Xianta Zhao, Hanli Key Laboratory of Intelligent Informatics for Safety and Emergency of Zhejiang Province Wenzhou University China Department of Computer Science Memorial University of Newfoundland St. John’s Canada State Key Laboratory for Novel Software Technology Nanjing University China College of Engineering and Computer Science Australian National University Australia

Blind face restoration aims to recover high-quality facial images from various unidentified sources of degradation, posing significant challenges due to the minimal information retrievable from the degraded images. Prior knowledge-based methods, leveraging geometric priors and facial features, have led to advancements in face restoration but often fall short of capturing fine details. To address this, we introduce a visual style prompt learning framework that utilizes diffusion probabilistic models to explicitly generate visual prompts within the latent space of pre-trained generative models. These prompts are designed to guide the restoration process. To fully utilize the visual prompts and enhance the extraction of informative and rich patterns, we introduce a style-modulated aggregation transformation layer. Extensive experiments and applications demonstrate the superiority of our method in achieving high-quality blind face restoration. The source code is available at https://***/LonglongaaaGo/*** Codes 68U10 © 2024, CC BY.

关键词： Generative adversarial networks