Downward Closed Language Generators

• We use downward closed languages for representing sets of states when performing forward reachability analysis on infinite-state systems. Downward closed languages are often more succinct than exact representations of the set of reachable states. We introduce a formalism for representing downward closed languages, called downward closed language generators (dlgs). We show that standard set operations needed for performing symbolic reachability analysis are computable for dlgs. Using a class of hierarchically defined dlgs, we have implemented a prototype for analysing timed Petri nets and used it to analyze a parameterized version of Fischer's protocol. We also show how dlgs can be used for uniform representation of formalisms previously presented for models such as Petri nets and lossy channel systems.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences (hsv//eng)

Publikations- och innehållstyp

vet (ämneskategori)

rap (ämneskategori)