{"controller"=>"catalog", "action"=>"show", "id"=>"274362978"}
  • EN
  • DA

Danish NationalResearch Database

  • Search Publications & Researchers
  • Open Access Indicator
  • Publications
  • Researchers
Example Finds records
water{} containing the word "water".
water supplies"{}" containing the phrase "water supplies".
author:"Doe, John"author:"{}" containing the prase "Doe, John" in the author field.
title:IEEEtitle:{} containing the word "IEEE" in the title field.
Need more help? Advanced search tutorial
  • Selected (0)
  • History

Refinement Checking on Parametric Modal Transition Systems

    • Save to Mendeley
    • Export to BibTeX
    • Export to RIS
    • Email citation
Authors:
  • Benes, Nikola ;
    Close
    FIMU
  • Kretínsky, Jan ;
    Close
    Technical University München
  • Larsen, Kim Guldstrand ;
    Close
    Department of Computer Science, The Technical Faculty of IT and Design, Aalborg University
  • Møller, Mikael Harkjær ;
    Close
    Department of Computer Science, The Technical Faculty of IT and Design, Aalborg University
  • Sickert, Salomon ;
    Close
    Technical University Munich (TUM)
  • Srba, Jiri
    Close
    Department of Computer Science, The Technical Faculty of IT and Design, Aalborg University
DOI:
10.1007/s00236-015-0215-4
Abstract:
Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS.
Type:
Journal article
Language:
English
Published in:
Acta Informatica, 2015, Vol 52, Issue 2, p. 269-297
Main Research Area:
Science/technology
Publication Status:
Published
Review type:
Peer Review
Submission year:
2015
Scientific Level:
Scientific
ID:
274362978

Full text access

  • Openaccess Elsewhere online
  • Doi Get publisher edition via DOI resolver
Checking for on-site access...

On-site access

At institution

  • Aalborg university.en

Metrics

Feedback

Sitemap

  • Search
    • Statistics
    • Tutorial
    • Data
    • FAQ
    • Contact
  • Open Access
    • Overview
    • Development
    • FAQ
    • Contact
  • About
    • Institutions
    • Release History
    • Cookies and privacy policy

Copyright © 1998–2018.

Fivu en