Min-max Computation Tree Logic

DOI10.1016/S0004-3702(01)00059-5MaRDI QIDQ5940962zbMATH OpenOpenAlexWikidataFDO

Authors Pallab Dasgupta, P. P. Chakrabarti, J. K. Deka, S. Sankaranarayanan

Publication date 20 August 2001

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0004-3702(01)00059-5

zbMATH Keywords

formal verificationmodel checkingtemporal logictiming verification

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

This paper introduces a branching time temporal query language called Min-max CTL which is similar in syntax to the popular temporal logic, CTL [\textit{E. M. Clarke, E. A. Emerson} and \textit{A. P. Sistla}, ACM Trans. Program. Lang. Systems 8, 244-263 (1986; Zbl 0591.68027)]. However unlike CTL, Min-max CTL can express timing queries on a timed model. We show that interesting timing queries involving a combination of min and max can be expressed in Min-max CTL. While model checking using most timed temporal logics is PSPACE-complete or harder [\textit{R. Alur} and \textit{T. A. Henzinger}, Inf. Comput. 104, No. 1, 35-77 (1993; Zbl 0791.68103); \textit{A. Alur, C. Courcoubetis} and \textit{D. Dill}, Inf. Comput. 104, No. 1, 2-34 (1993; Zbl 0783.68076)], we show that many practical timing queries, where we are interested in the worst-case or best-case timings, can be answered in polynomial time by querying the system using Min-max CTL.

Recommendations

• Min-max event-triggered computation tree logic
• Minimization of a search tree used in solving a system of logical equations
• Minimax trees in linear time with applications
• Minimax Trees in Linear Time with Applications
• scientific article; zbMATH DE number 1253054
• Minimum size tree-decompositions
• Minimum size tree-decompositions
• Minimax flow tree problems
• Minimax trees, paths, and cut sets
• Extended computation tree logic

Cites work

• A really temporal logic
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• scientific article; zbMATH DE number 3888913 (Why is no real title available?)
• scientific article; zbMATH DE number 5542185 (Why is no real title available?)
• scientific article; zbMATH DE number 177509 (Why is no real title available?)
• scientific article; zbMATH DE number 1423228 (Why is no real title available?)
• Model-checking in dense real-time
• Real-time logics: Complexity and expressiveness

Cited in

(7)

• Min-max event-triggered computation tree logic
• scientific article; zbMATH DE number 1670794 (Why is no real title available?)
• On solving temporal logic queries
• Model checking for a class of weighted automata
• Action and State Based Computation Tree Measurement Language and Algorithms
• A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria
• Collecting statistics over runtime executions

This page was built for publication: Min-max Computation Tree Logic

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