concurrency

Compositional Model Checking of Concurrent Systems

This paper presents a compositional framework to address the state explosion problem in model checking of concurrent systems. This framework takes as input a system model described as a network of communicating components in a high-level description …

Direct synthesis of timed circuits from free-choice STGs

Presents a new method to synthesize timed asynchronous circuits directly from the specification without generating a state graph. The synthesis procedure begins with a graph specification with timing constraints. A timing analysis extracts the timed …

Direct synthesis of timed asynchronous circuits

This paper presents a new method to synthesize timed asynchronous circuits directly from the specification without generating a state graph. The synthesis procedure begins with a deterministic graph specification with timing constraints. A timing …

Direct synthesis of timed asynchronous circuits

This paper presents a new method to synthesize timed asynchronous circuits directly from the specification without generating a state graph. The synthesis procedure begins with a deterministic graph specification with timing constraints. A timing …

POSET timing and its application to the synthesis and verification of gate-level timed circuits

This paper presents a new algorithm for timed state-space exploration, POSET timing, POSET timing improves upon geometric methods by utilizing concurrency and causality information to dramatically reduce the number of geometric regions needed to …

Verification of timed systems using POSETs

This paper presents a new algorithm for efficiently verifying timed systems. The new algorithm represents timing information using geometric regions and explores the timed state space by considering partially ordered sets of events rather than linear …