Formal Verification

← Back to Domain-Specific Abstractions by Domain

2 domain-specific abstractions whose origin domain is Formal Verification.

• Metric temporal logic — A temporal logic whose modalities carry quantitative time intervals, allowing formulas to require that events occur within explicit deadlines or durations.
• Reachability problem — The decision problem asking whether allowed transitions can carry a system from a specified initial state to a target state.