Tài liệu Regular Trace Event Structures doc

BRICS RS-96-32 P. S. Thiagarajan: Regular Trace Event Structures

Basic Research in Computer Science

BRICS

Regular Trace Event Structures

P. S. Thiagarajan

BRICS Report Series RS-96-32

ISSN 0909-0878 September 1996

Copyright c 1996, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work

is permitted for educational or research use

on condition that this copyright notice is

included in any copy.

See back inner page for a list of recent publications in the BRICS

Report Series. Copies may be obtained by contacting:

BRICS

Department of Computer Science

University of Aarhus

Ny Munkegade, building 540

DK - 8000 Aarhus C

Denmark

Telephone: +45 8942 3360

Telefax: +45 8942 3255

Internet: [email protected]

BRICS publications are in general accessible through World Wide

Web and anonymous FTP:

http://www.brics.dk/

ftp://ftp.brics.dk/pub/BRICS

Regular Trace Event Structures

P.S. Thiagarajan∗

BRICS†

Department of Computer Science

University of Aarhus

Ny Munkegade

DK-8000 Aarhus C, Denmark

September, 1996

Abstract

We propose trace event structures as a starting point for construct￾ing effective branching time temporal logics in a non-interleaved set￾ting. As a first step towards achieving this goal, we define the notion

of a regular trace event structure. We then provide some simple char￾acterizations of this notion of regularity both in terms of recognizable

trace languages and in terms of finite 1-safe Petri nets.

0 Introduction

This paper may be viewed as a first step towards the construction of effective

branching time temporal logics in a non-interleaved setting. We believe the

∗On leave from School of Mathematics, SPIC Science Foundation, Madras, India

†Basic Research In Computer Science,

Centre of the Danish National Research Foundation.

1