NDLI: Modular µ-Calculus Model-Checking with Formula-Dependent Hierarchical Abstractions

Please wait, while we are loading the content...

Studying the Interplay of Concurrency, Performance, Energy and Reliability with ArchOn -- An Architecture-Open Resource-Driven Cross-Layer Modelling Framework

Diagnosability under Weak Fairness

Testing Multithreaded Programs with Contextual Unfoldings and Dynamic Symbolic Execution

New Automatic Agent-Based Solutions for Feasible Reconfigurable MP-SoC Architectures

BenchKit, a Tool for Massive Concurrent Benchmarking

Sessions with an Unbounded Number of Agents

Parametrised Interface Automata

Modelling Data Processing for Interactive Scores Using Coloured Petri Nets

Author Index

Publisher's Information

2013 13th International Conference on Application of Concurrency to System Design

2012 12th International Conference on Application of Concurrency to System Design

2011 Eleventh International Conference on Application of Concurrency to System Design

2010 10th International Conference on Application of Concurrency to System Design

2009 Ninth International Conference on Application of Concurrency to System Design

2008 8th International Conference on Application of Concurrency to System Design

Seventh International Conference on Application of Concurrency to System Design (ACSD 2007)

Sixth International Conference on Application of Concurrency to System Design (ACSD'06)

Fifth International Conference on Application of Concurrency to System Design (ACSD'05)

Proceedings. Fourth International Conference on Application of Concurrency to System Design, 2004. ACSD 2004.

Third International Conference on Application of Concurrency to System Design, 2003. Proceedings.

Proceedings Second International Conference on Application of Concurrency to System Design

Proceedings 1998 International Conference on Application of Concurrency to System Design

Modular µ-Calculus Model-Checking with Formula-Dependent Hierarchical Abstractions

Content Provider	IEEE Xplore Digital Library
Author	Cornec, Yves-Stan Le Pommereau, Franck
Copyright Year	2014
Abstract	This paper defines a formal framework for the modular and hierarchical model-checking of mu-calculus against modular transitions systems. Given a formula phi, a module can be analysed alone, in such a way that the truth value of phi may be decided without the need to analyse other modules. If no conclusion can be drawn locally, the analysis provides information allowing to reduce the module to a smaller one that is equivalent with respect to the truth value of phi. This way, modules can be incrementally analysed, reduced and composed to other reduced modules until a conclusion is reached. On the one hand, modular analysis allows to avoid modules compositions and thus the corresponding combinatorial explosion, on the other hand, hierarchical analysis allows to reduce the modules that must be composed, which limits combinatorial explosion. Moreover, by proposing three complementary formula-dependent reductions, we expect better reductions than general approaches like bisimulation or tau reductions. The current paper is focused on defining the theoretical tools for this approach, finding interesting strategies to apply them efficiently is left to future work.
Starting Page	11
Ending Page	20
File Size	276218
Page Count	10
File Format	PDF
ISBN	9781479942817
ISSN	15504808
DOI	10.1109/ACSD.2014.14
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2014-06-23
Publisher Place	Tunisia
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Silicon Explosions Semantics Lattices Synchronization Tin Context Partial and incremental analysis Modular model-checking Hierarchical abstraction
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Compositional analysis of modular petri nets using hierarchical state space abstraction.

Model-checking an Epistemic µ-calculus with Synchronous and Perfect Recall Semantics

Modular Verification of Synchronous Programs

Simulation-based abstractions for software product-line model checking

Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement

Reducing State Explosion with Context Modeling for Model-Checking

Abstractions from proofs

Compositional Abstraction Refinement for Timed Systems

Modular proof systems for partial functions with Evans equality (2006)

Modular µ-Calculus Model-Checking with Formula-Dependent Hierarchical Abstractions

Similar Documents

Compositional analysis of modular petri nets using hierarchical state space abstraction.

Model-checking an Epistemic µ-calculus with Synchronous and Perfect Recall Semantics

Modular Verification of Synchronous Programs

Simulation-based abstractions for software product-line model checking

Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement

Reducing State Explosion with Context Modeling for Model-Checking

Abstractions from proofs

Compositional Abstraction Refinement for Timed Systems

Modular proof systems for partial functions with Evans equality (2006)

Modular µ-Calculus Model-Checking with Formula-Dependent Hierarchical Abstractions