Circular Hierarchical Reasoning using Past Time LTL

Loading...
Thumbnail Image

View/Download File

Persistent link to this item

Statistics
View Statistics

Journal Title

Journal ISSN

Volume Title

Title

Circular Hierarchical Reasoning using Past Time LTL

Published Date

2011

Publisher

University of Minnesota

Type

Report

Abstract

We describe a composition rule for hierarchically composed components that may involve circular reasoning between the components. It is similar to previous work by McMillan, specialized to component level reasoning. In contrast to McMillan's work, our composition rule can be used in provers that only support safety properties (e.g. k-induction model checkers) as long as the system and component contracts consist of state invariants. The composition rule still holds for richer contracts, but the resulting verification conditions then require a general purpose model checker.

Keywords

Description

Associated research group: Critical Systems Research Group

Related to

Replaces

License

Series/Report Number

Funding information

Isbn identifier

Doi identifier

Previously Published Citation

Department of Computer Science and Engineering University of Minnesota 200 Union St. Minneapolis, MN 55455

Other identifiers

Suggested citation

Cofer, Darren; Gacek, Andrew; Whalen, Michael. (2011). Circular Hierarchical Reasoning using Past Time LTL. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/217402.

Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.