A method for analyzing properties of hierarchical predicate transition nets

Author

He, Xudong

Author_Institution

Dept. of Comput. Sci., North Dakota State Univ., Fargo, ND, USA

fYear

1995

fDate

9-11 Aug 1995

Firstpage

50

Lastpage

55

Abstract

Hierarchical high level Petri nets have been proposed in recent years as a powerful formal method for modeling large concurrent and distributed systems but they are even more difficult to analyze than flat high level Petri nets, which are also lacking effective analysis methods themselves. A method for analyzing properties of hierarchical predicate transition Petri nets is proposed. The method employs two temporal induction techniques, one for safety properties and the other for liveness properties, without using temporal logic formalism. Within each induction technique, a hybrid reasoning technique combining net structural and behavioral reasoning, and ordinary first order logic reasoning is used

Keywords

Petri nets; distributed processing; formal logic; inference mechanisms; behavioral reasoning; distributed systems modelling; first order logic reasoning; formal method; hierarchical high level Petri nets; hierarchical predicate transition Petri nets; hierarchical predicate transition nets; hybrid reasoning technique; liveness properties; net structural reasoning; safety properties; temporal induction techniques; Algebra; Board of Directors; Concurrent computing; Encapsulation; Fires; Labeling; Solids; Tail; Tin;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Software and Applications Conference, 1995. COMPSAC 95. Proceedings., Nineteenth Annual International

Conference_Location

Dallas, TX

ISSN

0730-3157

Print_ISBN

0-8186-7119-X

Type

conf

DOI

10.1109/CMPSAC.1995.524757

Filename

524757