For the most recent entries see the Petri Nets Newsletter.

LTrL based model checking for a restricted class of Signal Transition Graphs.

Meyer, R.; Thiagarajan, P.S.

In: Proc. 2nd Workshop on Hardware Design and Petri Nets (HWPN'99) of the 20th Int. Conf. on Application and Theory of Petri Nets (PN'99), 21 June 1999, Williamsburg, VA, pages 3-14. 1999.

Also in: Yakovlev, A.; Gomes, L.; Lavagno, L.: Hardware Design and Petri Nets, pages 93-106. Boston: Kluwer Academic Publishers, 2000.

Abstract: The paper shows that the linear time temporal logic (LTrL) can be used as a specification mechanism for restricted signal transition nets. The logic LTrL is interpreted over the finite prefixes of Mazurkiewicz traces. Mazurkiewicz traces are restricted labeled transition orders which constitute an elegant and powerful extension of the notion of a sequence. The theory of traces is rich and well-understood. Among the logics for traces, LTrL occupies a special position in that it has exactly the same expressive power as the first order theory of traces. Due to the classic theorem of Kamp, later strengthened by Gabbay at al., this matches the expressive power of LTL, the linear time temporal logic formulated by Pnueli in a sequential setting.

Keywords: linear logics, model checking, signal transition graphs.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography