On refinements of Boolean and parametric modal transition systems

DOI10.1007/978-3-642-39718-9_13MaRDI QIDQ2851908zbMATH OpenOpenAlexFDO

Authors Jan Křetínský, Salomon Sickert

Publication date 4 October 2013

Published in Theoretical Aspects of Computing – ICTAC 2013 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1304.5278

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We consider the extensions of modal transition systems (MTS), namely Boolean MTS and parametric MTS and we investigate the refinement problems over both classes. Firstly, we reduce the problem of modal refinement over both classes to a problem solvable by a QBF solver and provide experimental results showing our technique scales well. Secondly, we extend the algorithm for thorough refinement of MTS providing better complexity then via reductions to previously studied problems. Finally, we investigate the relationship between modal and thorough refinement on the two classes and show how the thorough refinement can be approximated by the modal refinement.

Recommendations

• Refinement checking on parametric modal transition systems
• Parametric modal transition systems
• On Modal Refinement and Consistency
• Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete
• EXPTIME-completeness of thorough refinement on modal transition systems

Cited in

(11)

• An inductive approach for modal transition system refinement
• EXPTIME-completeness of thorough refinement on modal transition systems
• Refinement checking on parametric modal transition systems
• A refinement repair algorithm based on refinement game for KMTS models
• Coherent modal transition systems refinement
• Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete
• Refinement is complete for implementations
• Parametric modal transition systems
• Topological analysis of refinement
• On Modal Refinement and Consistency
• Modal transition system encoding of featured transition systems

Describes a project that uses

Uses Software

• MIO Workbench
• JML

This page was built for publication: On refinements of Boolean and parametric modal transition systems

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