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

Journal of Applied Logics 2021年第10期8卷 2447-2470页

作者： Bentkamp, Alexander Vrije Universiteit Amsterdam Netherlands State Key Lab. of Computer Science Institute of Software CAS Beijing China

The embedding path order, introduced in this article, is a variant of the recursive path order (RPO) for untyped λ-free higher-order terms (also called applicative first-order terms). Unlike other higher-order variants of RPO, it is a ground-total and well-founded simplification order, making it more suitable for the superposition calculus. I formally proved the order’s theoretical properties in Isabelle/HOL and evaluated the order in a prototype based on the superposition prover Zipperposition. © 2021, College Publications. All rights reserved.

关键词： Embeddings

来源：评论

学校读者我要写书评

暂无评论

Long- and Short- Term Sequential Recommendation with Temporal Interval

Long- and Short- Term Sequential Recommendation with Tempora...

引用

Symposia and Workshops on Ubiquitous, Autonomic and Trusted Computing, UIC-ATC

作者： Kun He Qiyan Liu Qianmu Li Shunmei Meng Nanjing University of Science and Technology Nanjing China Computer Engineering University of Toronto State Key Lab. for Novel Software Technology Nanjing University Nanjing China

Sequential recommendation aims to learn the changes of users’ interests according to their historical behaviors and predict the most likely next item. Since user’s historical behavior are sequential actions, user’s interest in different time periods has different emphases. For predicting a user’s next item, not only the recent behavior is important, but also long-term preference with all historical behaviors could not be ignored. Recently, self-attention based user preference modeling has drawn much attention for its advantages of fewer parameters and parallelism. However, most of the existing self-attention based model do not make a good distinction between the long-term and short-term preferences of users. Based on the observations, we design a sequential recommendation model based on a combination of long-term and short-term preference. On the one hand, considering the changes of users’ interests in different periods, we divide the sequence of users’ behaviors into different temporal windows. Then, we use GRU to capture users’ interests in different temporal window. On the other hand, to better combine the global and local information of user’s, we adopt a locally constrained multi-head attention mechanism based on Transformer encoder. On three real-world public datasets, we finally validate the efficacy of our method.

关键词：

来源：评论

学校读者我要写书评

暂无评论

A Generalized Hybrid Hoare Logic

arXiv

引用

arXiv 2023年

作者： Zhan, Naijun Jin, Xiangyu Zhan, Bohua Wang, Shuling Guelev, Dimitar School of Computer Science Peking University Institute of Software Chinese Academy of Sciences Beijing China State Key Lab. of Computer Science Institute of Software Chinese Academy of Sciences University of CAS Beijing China Huawei Technologies Co. Ltd. Beijing China National Key Laboratory of Space Integrated Information System Institute of Software Chinese Academy of Sciences University of CAS Beijing China Institute of Mathematics and Informatics Bulgarian Academy of Sciences Sofia Bulgaria

Deductive verification of hybrid systems (HSs) increasingly attracts more attention in recent years because of its power and scalab.lity, where a powerful specification logic for HSs is the cornerstone. Often, HSs are naturally modelled by concurrent processes that communicate with each other. However, existing specification logics cannot easily handle such models. In this paper, we present a specification logic and proof system for Hybrid Communicating Sequential Processes (HCSP), that extends CSP with ordinary differential equations (ODE) and interrupts to model interactions between continuous and discrete evolution. Because it includes a rich set of algebraic operators, complicated hybrid systems can be easily modelled in an algebra-like compositional way in HCSP. Our logic can be seen as a generalization and simplification of existing hybrid Hoare logics (HHL) based on duration calculus (DC), as well as a conservative extension of existing Hoare logics for concurrent programs. Its assertion logic is the first-order theory of differential equations (FOD), together with assertions about traces recording communications, readiness, and continuous *** prove continuous relative completeness of the logic w.r.t. FOD, as well as discrete relative completeness in the sense that continuous behaviour can be arbitrarily approximated by discretization. Finally, we implement the above logic in Isabelle/HOL, and apply it to verify two case studies to illustrate the power and scalab.lity of our logic. Copyright © 2023, The Authors. All rights reserved.

关键词： Scalab.lity

来源：评论

学校读者我要写书评

暂无评论

Model Predictive Control with Reach-avoid Analysis

arXiv

引用

arXiv 2023年

作者： Ren, Dejin Lu, Wanli Lv, Jidong Zhang, Lijun Xue, Bai State Key Lab. of Computer Science Institute of Software CAS Beijing China University of Chinese Academy of Sciences Beijing China National Engineering Research Center of Rail Transportation Operation and Control System Beijing Jiaotong University Beijing China

In this paper we investigate the optimal controller synthesis problem, so that the system under the controller can reach a specified target set while satisfying given constraints. Existing model predictive control (MPC) methods learn from a set of discrete states visited by previous (sub-)optimized trajectories and thus result in computationally expensive mixed-integer nonlinear optimization. In this paper a novel MPC method is proposed based on reach-avoid analysis to solve the controller synthesis problem iteratively. The reach-avoid analysis is concerned with computing a reach-avoid set which is a set of initial states such that the system can reach the target set successfully. It not only provides terminal constraints, which ensure feasibility of MPC, but also expands discrete states in existing methods into a continuous set (i.e., reach-avoid sets) and thus leads to nonlinear optimization which is more computationally tractable online due to the absence of integer variables. Finally, we evaluate the proposed method and make comparisons with state-of-the-art ones based on several examples. Copyright © 2023, The Authors. All rights reserved.

关键词： Model predictive control

来源：评论

学校读者我要写书评

暂无评论

Bridge the Gap between Supervised and Unsupervised Learning for Fine-Grained Classification

SSRN

引用

SSRN 2023年

作者： Wang, Jiabao Li, Yang Wei, Xiu-Shen Li, Hang Miao, Zhuang Zhang, Rui Army Engineering University of PLA Jiangsu Nanjing210007 China PCA Lab Key Lab of Intelligent Perception and Systems for High-Dimensional Information of Ministry of Education Jiangsu Key Lab of Image and Video Understanding for Social Security School of Computer Science and Engineering Nanjing University of Science and Technology Jiangsu Nanjing210094 China State Key Lab. for Novel Software Technology Nanjing University Jiangsu Nanjing210023 China

Unsupervised learning technology has caught up with or even surpassed supervised learning technology in general object classification (GOC) and person re-identification (re-ID). However, it is found that the unsupervised learning of fine-grained visual classification (FGVC) is more challenging than GOC and person re-ID. In order to bridge the gap between unsupervised and supervised learning for FGVC, we investigate the essential factors for the performance gap. Furthermore, we propose a simple, effective, and practical method, termed as UFCL, to alleviate the gap. Three key issues are concerned and improved: First, we introduce a robust and powerful backbone, ResNet50-IBN, which has an ability of domain adaptation when we transfer ImageNet pre-trained models to FGVC tasks. Next, we propose to introduce HDBSCAN inst.ad of DBSCAN to do clustering, which can generate better clusters for adjacent categories with fewer hyper-parameters. Finally, we propose a weighted feature agent and its updating mechanism to do contrastive learning, which can improve the optimization process of learning the parameters of the network. The effectiveness of our UFCL is verified on four public FGVC datasets. Under the unsupervised FGVC setting, we achieve state-of-the-art results, and analyze the key factors and the important parameters to provide a practical guidance. © 2023, The Authors. All rights reserved.

关键词： Image classification

来源：评论

学校读者我要写书评

暂无评论

Knowledge-aware Multi-view Cross Learning for Edge-based Collab.rative Recommendation

Knowledge-aware Multi-view Cross Learning for Edge-based Col...

引用

International Conference on Parallel and Distributed Systems (ICPADS)

作者： Yang Dai Shunmei Meng Huanhuan Gu Nan Liu Longchuan Tu School of Cyberspace Security NanJing University of Science and Technology Nanjing China State Key Lab. for Novel Software Technology NanJing University Nanjing China Department of Computer Science and Engineering NanJing University of Science and Technology Nanjing China Nanjing Sinovatio Technology Co. Ltd. Nanjing China

In order to effectively overcome the sparsity and cold start challenges of collab.rative filtering in actual scenarios, and provide more accurate suggestions, knowledge graphs are commonly utilized in recommender systems. Graph neural networks are increasingly used in knowledge graph-based recommender systems. Nevertheless, conventional recommender systems overlook the relationship information between items and entities as well as the sparse supervision signal, potentially leading to a decline in the actual recommendation performance. In this investigation, we propose KMCL, a Knowledge-aware Multi-view Cross-learning framework for edge-based collab.rative recommendation. In contrast to the typical manner of dealing with knowledge graphs, our approach investigates three different graph views to improve users’ and items’ embedding representations, respectively. Firstly, the merged user-item KG graph is utilized to integrate the multi-hop neighbor information of each user, with the Graph Attention Network assigning various weights to different neighbors. Secondly, Graph Neural Network collects the top-x neighbor nodes for learning in the collab.rative view of user-item graph and item-entity graph. Finally, a cross module is developed to share high-level information between embeddings with the same features. In addition, we also introduce the idea of edge computing, which preprocesses and calculates the locally obtained user preferences first, and then inputs them into different views to improve the recommendation efficiency. Experimental results demonstrate that KMCL delivers better suggestions than state-of-the-art baseline models in delivering superior recommendations. Furthermore, our approach maintains higher accuracy in predicting outcomes in less familiar interaction scenarios.

关键词：

来源：评论

学校读者我要写书评

暂无评论

MACRO: Incentivizing Multi-Leader Game-Based Pareto-Efficient Crowdsourcing for Video Analytics

MACRO: Incentivizing Multi-Leader Game-Based Pareto-Efficien...

引用

International Conference on Data Engineering

作者： Yu Chen Sheng Zhang Ziying Zhou Xiaokun Wang Yu Liang Ning Chen Yuting Yan Mingjun Xiao Jie Wu Zhuzhong Qian Harry Xu State Key Lab. for Novel Software Technology Nanjing University P.R. China School of Systems Science Beijing Normal University China School of Computer and Electronic Information / School of Artificial Intelligence Nanjing Normal University China School of Computer Science and Technology University of Science and Technology of China P.R. China Center for Networked Computing Temple University USA Computer Science Department Samueli School of Engineering University of California Los Angeles USA

ISBN: (数字)9798350317152

ISBN: (纸本)9798350317169

In recent years, many crowdsourcing platforms have emerged, using the resources of recruited workers to perform diverse outsourcing tasks, where the video analytics attracts much attention due to its practical implications. For maximum profits, platforms carefully choose the workers and determine the video analytics configurations to ensure accuracy; meanwhile, workers possess the flexibility to tailor the configurations for their indivi-dual gains, which makes it hard for platforms to optimize their profits considering the platform-worker conflicts. In this paper, we design an incentive mechanism for Multi-leader game-based video Analytics upon CROwdsourcing, named MACRO, to over-come the above situation. Under that mechanism, we first formu-late the utility optimization problems for platforms and workers, respectively. We then propose a dual ascent-based method to op-timally determine the video analytics configurations for a multi-platform game, ensuring Pareto efficiency. Moreover, in the context of a multi-leader game involving platform-worker conflicts, we design an incentive function with its incentive factor update strategy and propose an ADMM-based approach for maximizing incentives that motivate workers to contribute to the platforms' profits. Rigorous proofs demonstrate the linear convergence of the MACRO to the multi-leader Stackelberg equilibrium. Trace-driven experiments show that MACRO improves the Pareto efficiency by 26.3%, outperforming other approaches.

关键词： Crowdsourcing Accuracy Visual analytics Games Data engineering Outsourcing Task analysis

来源：评论

学校读者我要写书评

暂无评论

Reach-Avoid Analysis for Polynomial Stochastic Differential Equations

arXiv

引用

arXiv 2022年

作者： Xue, Bai Zhan, Naijun Fränzle, Martin State Key Lab. of Computer Science Institute of Software CAS Beijing China University of Chinese Academy of Sciences CAS Beijing China Carl von Ossietzky Universität Oldenburg Germany

In this paper we propose a novel semi-definite programming approach that solves reach-avoid problems over open (i.e., not bounded a priori) time horizons for dynamical systems modeled by polynomial stochastic differential equations. The reach-avoid problem in this paper is a probabilistic guarantee: we approximate from the inner a p-reach-avoid set, i.e., the set of initial states guaranteeing with probability larger than p that the system eventually enters a given target set while remaining inside a specified safe set till the target hit. Our approach begins with the construction of a bounded value function, whose strict p super-level set is equal to the p-reach-avoid set. This value function is then reduced to a twice continuously differentiable solution to a system of equations. The system of equations facilitates the construction of a semi-definite program using sum-of-squares decomposition for multivariate polynomials and thus the transformation of nonconvex reach-avoid problems into a convex optimization problem. The semi-definite program can be solved efficiently in polynomial time with many existing powerful algorithms such as interior point methods and off-the-shelf software packages. We would like to point out that our approach can straightforwardly be specialized to address classical safety verification by, a.o., stochastic barrier certificate methods and reach-avoid analysis for ordinary differential equations. In addition, several examples are provided to demonstrate theoretical and algorithmic developments of the proposed method. Copyright © 2022, The Authors. All rights reserved.

关键词： Ordinary differential equations

来源：评论

学校读者我要写书评

暂无评论

Dynamic Detection of AsyncTask Related Defects

Dynamic Detection of AsyncTask Related Defects

引用

IEEE International Conference on software Quality, Reliability and Security (QRS)

作者： Qing Liu Linjie Pan Baoquan Cui Jun Yan Jian Zhang State Key Lab. of Computer Science Institute of Software CAS University of Chinese Academy of Sciences Technology Center of Software Engineering Institute of Software CAS

ISBN: (纸本)9781665458146

As a widely used Android asynchronous component, AsyncTask is used to run time-consuming tasks. However, the misuse of AsyncTask will cause defects, i.e., crashes and memory leaks. Based on static analysis, existing approaches cannot accurately detect AsyncTask-related defects and produce many false positives since some paths are not reachable in practice. In this paper, we propose a dynamic detection method based on inst.umentation, Monkey execution and log analysis to detect these defects. And we implement a tool AD2Checker based on the proposed method. Our experiment on 19 real-world apps shows that it has found 145 bugs and has no false positives. Moreover, it triggers crashes caused by misuse of AsyncTask.

关键词： Printing inst.uments Conferences computer bugs Static analysis software quality software reliability

来源：评论

学校读者我要写书评

暂无评论

Outer-approximating Controlled Reach-avoid Sets for Polynomial Systems

Outer-approximating Controlled Reach-avoid Sets for Polynomi...

引用

IEEE Conference on Decision and Control

作者： Changyuan Zhao Chuchu Fan Bai Xue State Key Lab. of Computer Science Institute of Software Chinese Academy of Sciences Beijing China University of Chinese Academy of Sciences Beijing China Department of Aeronautics and Astronautics MIT U.S.

ISBN: (数字)9781665467612

ISBN: (纸本)9781665467629

In this paper we propose a semi-definite programming method for computing outer-approximations (i.e., super-sets) of controlled reach-avoid sets of discrete-time polynomial systems subject to control inputs. The controlled reach-avoid set is a set of all initial states that there exists at least one control policy which steers the system starting from each of them to enter a specified target set in finite time while avoiding a given unsafe set till the target is hit. First, a Bellman type equation, whose unique bounded solution can characterize the exact controlled reach-avoid set, is derived. By relaxing this equation, a set of quantified inequalities for outer-approximating the controlled reach-avoid set is obtained. Via comparing to a set of constraints in state-of-the-art methods on occupation measures, we find that each has its own strengths and can complement each other in outer-approximating controlled reach-avoid sets. As a consequence, we integrate them and obtain a new set of constraints, which is weaker and thus contributes to the gain of tighter outer-approximations. The resulting set of constraints can be encoded into a semi-definite program via the sum-of-squares decomposition for multivariate variables, which can be solved efficiently via interior point methods in polynomial time. Finally, several examples demonstrate the benefits of our method on gaining tighter outer-approximations of controlled reach-avoid sets over existing methods.

关键词： Programming Control systems

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：