Recogizing safety and liveness

A formal characterization for safety properties and liveness properties is given in terms of the structure of the Buchi automaton that specifies the property. The characterizations permit a property to be decomposed into a safety property and a liveness property whose conjunction is the original. Th...

Full description

Bibliographic Details
Main Author: Alpern, Bowen
Other Authors: Schneider, Fred B.
Format: Electronic Article
Language:English
Subjects:
Online Access:Texto completo

MARC

LEADER 00000nma a22000007a 4500
003 AR_CdUFM
005 20210830212140.0
006 m|||||o||d||00| 0
007 cr |||||||||||
008 s1987 us||| |o||||||0| | eng||
040 |a AR_CdUFM   |b spa 
041 |a eng 
100 1 |9 24834  |a Alpern, Bowen 
245 1 0 |a Recogizing safety and liveness  |h [recurso electrónico] /  |c Bowen Alpern and Fred B. Schneider. 
300 |a 1 recurso en línea (p. 117-126) 
520 |a A formal characterization for safety properties and liveness properties is given in terms of the structure of the Buchi automaton that specifies the property. The characterizations permit a property to be decomposed into a safety property and a liveness property whose conjunction is the original. The characterizations also give insight into techniques required to prove a large class of safety and liveness properties. 
650 4 |a Liveness 
650 4 |a Computación 
650 4 |a Safety 
700 |9 15421  |a Schneider, Fred B. 
773 |g No. 2 (1987)  |t Distributed computing 
856 |u https://www.cs.cornell.edu/fbs/publications/RecSafeLive.pdf  |y Texto completo 
942 |2    |c ARTDEREVL 
945 |a MEG  |d 2021-08-30 
952 |0 0  |1 0  |2    |4 0  |6 ARTÍCULO_DE_REVISTA_EN_LÍNEA  |7 0  |9 45025  |a MMA  |b MMA  |c Recurso en línea  |d 2021-08-30  |o Artículo de Revista en Línea  |p ARL0023  |r 2021-08-30 00:00:00  |u https://www.cs.cornell.edu/fbs/publications/RecSafeLive.pdf  |w 2021-08-30  |y ARTDEREVL 
999 |c 20603  |d 20601