Rules for abstraction

DOI10.1007/3-540-63875-X_41MaRDI QIDQ4370347zbMATH OpenFDO

Authors Stephan Merz

Publication date 10 November 1998

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-63875-X_41

zbMATH Keywords

homomorphic abstractioninteractive theorem provingmodel checkingtemporal logic of actionsTLA

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45)

Review text

The paper aims at a logical reconstruction of the principle of homomorphic abstraction, the investigation being performed from both theoretical and practical points of view. The TLA is used mainly because its distinction between the transition and temporal levels of description offers an adequate framework for combining interactive theorem proving and model checking. The contribution of the paper is twofold: to re-examine the principles underlying abstraction techniques by stating a series of proof rules in Lamport's TLA and to generalize known abstraction techniques using the standard laws of temporal logic. A brief overview of TLA and the main proof rules for abstraction and an illustrative example are given in the first four sections of the paper. Section five discusses techniques to obtain better abstractions, followed by comments. A comparative analysis with already existing work is supplied in the final part of the paper. For the entire collection see [Zbl 0878.00079].

Recommendations

• Abstraction and abstraction refinement
• scientific article; zbMATH DE number 2110619
• scientific article; zbMATH DE number 2102725
• Abstraction and Refinement in Model Checking
• Abstraction as the key for invariant verification

Cited in

(6)

• Which Abstraction Principles are Acceptable? Some Limitative Results
• Lumpability abstractions of rule-based systems
• Structural-Abstraction Principles
• Functional and Logic Programming
• Correct Hardware Design and Verification Methods
• 50 Shades of Rule Composition

This page was built for publication: Rules for abstraction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4370347)