Infinite-state high-level MSCs: model-checking and realizability

DOI10.1016/J.JCSS.2005.09.007zbMATH Open1105.68071OpenAlexW2146742781MaRDI QIDQ2495403FDOQ2495403

Authors: Blaise Genest, Anca Muscholl, Helmut Seidl, Marc Zeitoun 

Publication date: 30 June 2006

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jcss.2005.09.007

Recommendations

• scientific article; zbMATH DE number 2086660
• scientific article; zbMATH DE number 1754631
• scientific article; zbMATH DE number 1927562
• Realizability of high-level message sequence charts: closing the gaps
• scientific article; zbMATH DE number 1701776

zbMATH Keywords

synthesisconcurrencycommunicating automataMSC model-checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• On Communicating Finite-State Machines
• On recognizable subsets of free partially commutative monoids
• Realizability and verification of MSC graphs
• Title not available (Why is that?)
• Title not available (Why is that?)
• SYNTHESIZING STATE-BASED OBJECT SYSTEMS FROM LSC SPECIFICATIONS
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Developments in Language Theory

Cited In (22)

• Tools and Algorithms for the Construction and Analysis of Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Fundamental Approaches to Software Engineering
• Bounded MSC communication
• Dynamic communicating automata and branching high-level MSCs
• Automated verification of automata communicating via FIFO and bag buffers
• Shared-memory systems and charts
• Synthesis and Analysis of Petri Nets from Causal Specifications
• High-level message sequence charts and projections.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Comparing channel restrictions of communicating state machines, high-level message sequence charts, and multiparty session types
• Causal message sequence charts
• Title not available (Why is that?)
• Realizability Criteria for Compositional MSC
• The Synthesis Problem of Netcharts
• Title not available (Why is that?)
• Synthesis of Safe Message-Passing Systems

This page was built for publication: Infinite-state high-level MSCs: model-checking and realizability

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