检索结果-南通市图书馆

维普期刊数据库

Macro liveness graph and liveness of ω-independent unbounded nets

在线全文

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2015年第3期58卷 132-141页

作者： WANG ShouGuang GAN MengDi ZHOU MengChu School of Information and Electronic Engineering Zhejiang Gongshang University Key Laboratory of Embedded System and Service Computing Ministry of EducationTongji University Department of Electrical and Computer Engineering New Jersey Institute of Technology

liveness is a basic property of a system and the liveness issue of unbounded Petri nets remains one of the most difficult problems in this *** work proposes a novel method to decide the liveness of a class of unbounded generalized Petri nets calledω-independent unbounded nets,breaking the existing limits to one-place-unbounded *** algorithm to construct a macro liveness graph(MLG)is developed and a critical condition based on MLG deciding the liveness ofω-independent unbounded nets is *** are provided to demonstrate its effectiveness.

关键词： discrete event system(DES) Petri nets complex systems liveness property analysis

A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2019年第1期13卷 51-72页

作者： Kazuhiro OGATA School of Information Science Japan Advanced Institute of Science and Technology (JAIST) 1-1 AsahidaiNomiIshikawa 923-1292Japan

This paper proposes an approach to making livehess model checking problems under fairness *** proposed method divides such a problem into smaller ones that can be *** is not superior to existing tools dedicated to model checking liveness properties under fairness assumptions in terms of model checking performance but has the following positive aspects:1)the approach can be used to model check liveness properties under anti-fairness assumptions as well as fairness assumptions,2)the approach can help humans better understand the reason why they need to use fairness and/or anti-fairness assumptions,and 3)the approach makes it possible to use existing linear temporal logic model checkers to model check liveness properties under fairness and/or anti-fairness assumptions.

关键词： anti-fairness fairness liveness property Maude model checking

Notes on liveness and Boundedness of Extended Strong Asymmetric Choice Nets Ⅱ

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2001年第5期16卷 426-433页

作者：焦莉陆维明 DivisionofComputerScience InstituteofMathematicsAcademyofMathematicsandSystemScienceTheChineseAcademyofSciencesBeijing100080P.R.China DivisionofComputerScience InstituteofMath

In this paper, the Extended Strong Asymmetric Choice Nets Ⅱ (ESACN Ⅱ), a subclass of Asymmetric Choice Nets (ACN) including Extended Free Choice Nets (EFCN) and Strong Asymmetric Choke Nets Ⅱ (SACN Ⅱ, is presented. A necessary and sufficient condition for liveness of ESACN Ⅱ is proposed. Moreover, a criterion is introduced, which is necessary and sufficient for judgement of liveness and boundedness of ESACN Ⅱ. Meanwhile a polynomial time algorithm is given to decide liveness and boundedness for ESACN Ⅱ.

关键词： asymmetric choice net (ACN) extended strong asymmetric choice nets Ⅱ (ESACN Ⅱ) liveness boundedness algorithm polynomial time

维普期刊数据库

Boundedness and liveness enforcement for labeled Petri nets using transition priority

在线全文

学校读者我要写书评

暂无评论

Journal of Electronic Science and Technology 2023年第4期21卷 75-90页

作者： Ye-Jia Liu Xun-Bo Li School of Mechanical and Electrical Engineering University of Electronic Science and Technology of ChinaChengdu611731China

This paper deals with the supervisory control problem of discrete event systems modeled by labeled Petri nets. The system is originally unbounded. First, the solvability of the problem is confirmed. A necessary condition is given and proven for the existence of a feasible priority-based controller based on the notions of liveness and transition invariants. Next, a cyclic behavior graph is constructed, which shows the reachable markings that guarantee the maximum liveness of the system within a given bound vector. Finally, an on-line control strategy is proposed to enforce boundedness and liveness to the given system by appending priority relations to transitions. The dynamic priority relation changes flexibly according to the current state of the system and enforces the system evolving in a bounded and live manner. In addition, numerical examples are studied to verify the validity of the proposed approach that remains the structure of the plant net and is efficient for on-line control.

关键词： Boundedness Control strategy liveness Petri nets Priority Transition invariant

liveness characterization for GFC systems(Ⅰ)

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Science China(Technological Sciences) 1996年第2期39卷 196-205页

作者：曹存根 Institute of Computing Technology Chinese Academy of SciencesBeijing 100080China

The significant features concerning liveness of generalized free-choice (GFC) systems are *** features provide a sound basis for analyzing liveness of GFC systems in a reductive *** is interesting is that the characterization is just based on deadlocks,rather than on both deadlocks and traps as Commoner characterizes the liveness of ordinary free-choice *** proof techniques for proving liveness-related features of GFC systems are introduced.

关键词： free-choice net liveness generalized free-choice net

维普期刊数据库

Specification and Verification of Multimedia Synchronization in Duration Calculus

在线全文

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2003年第2期18卷 172-180页

作者：马华东 SchoolofComputerScienceandTechnologyBeijingUniversityofPostsandTelecommunications Beijing100876P.R.C

This paper proposes a new method of specifying multimedia synchronization basedon Duration Calculus (DC), a real time interval logic, presents the completeness of the new model,and uses it to specify the temporal relations between multimedia objects. Moreover, the paperprovides a method of constructing a meta-script based on basic synchronization requirements. Someproperties of the formal specifications, including safety and liveness, are stated in DC. Furthermore,the verification of the above properties is discussed in DC semantic. Compared with other methodsfor specifying multimedia synchronization, this method is more powerful and flexible, and it is goodat specifying the quantitative properties of multimedia synchronization.

关键词： liveness safety temporal synchronization duration calculus multimedia

Manufacturing System Design Using Augmented Marked Graph

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Manufacturing System Design Using Augmented Marked Graph

第二十四届中国控制会议

作者： K.S.Cheung K.O.Chow SCE Hong Kong Baptist University Kowloon Department of Computer Science City University of Hong Kong Kowloon

＜正＞ Augmented marked graphs have a number of known properties pertaining to their liveness and reversibility. In this paper, we show the application of augmented marked graphs to manufacturing system design. By modelling a manufacturing system using an augmented marked graph, the system liveness and reversibility can be effectively analysed based on the properties of augmented marked graphs.

关键词： Manufacturing system augmented marked graph Petri net liveness reversibility.

来源： cnki会议评论

在线全文

cnki会议

学校读者我要写书评

暂无评论

“现场性”与“媒介化”：媒介时代的剧场