Deciding safety properties in infinite-state pi-calculus via behavioural types

DOI10.1016/J.IC.2012.01.006zbMATH Open1279.68192OpenAlexW1984379137MaRDI QIDQ418155FDOQ418155

Authors Lucia Acciai, Michele Boreale

Publication date 24 May 2012

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2012.01.006

zbMATH Keywords

decidabilitypi-calculusbehavioural typessafetyspatial logic

Mathematics Subject Classification ID

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

Recommendations

• Deciding Safety Properties in Infinite-State Pi-Calculus via Behavioural Types
• Spatial and behavioral types in the pi-calculus
• Spatial and Behavioral Types in the Pi-Calculus
• Using session types for reasoning about boundedness in the \(\pi\)-calculus
• Using session types for reasoning about boundedness in the \(\pi\)-calculus

Cites work

• scientific article; zbMATH DE number 1809622 (Why is no real title available?)
• scientific article; zbMATH DE number 4030997 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 2163033 (Why is no real title available?)
• scientific article; zbMATH DE number 3310089 (Why is no real title available?)
• A generic type system for the pi-calculus
• A logic you can count on
• A spatial logic for concurrency. I
• A theory of structural stationarity in the \(\pi\)-calculus
• Algorithmic analysis of programs with well quasi-ordered domains.
• Anytime, anywhere: modal logics for mobile ambients
• Automata, Languages and Programming
• Deciding Safety Properties in Infinite-State Pi-Calculus via Behavioural Types
• Deciding validity in a spatial logic for trees
• Expressiveness and complexity of graph logic
• Forward Analysis for WSTS, Part II: Complete WSTS
• Forward analysis for WSTS. I: Completions
• Foundations of Software Science and Computation Structures
• Logical Semantics of Types for Concurrency
• Model checking mobile ambients
• On the Expressive Power of Restriction and Priorities in CCS with Replication
• On the Relationship between π-Calculus and Finite Place/Transition Petri Nets
• On the relationship between spatial logics and behavioral simulations
• Ordering by Divisibility in Abstract Algebras
• Reduction and covering of infinite reachability trees
• Spatial and behavioral types in the pi-calculus
• Spatial-Behavioral Types, Distributed Services, and Resources
• The complexity of theorem-proving procedures
• The name discipline of uniform receptiveness
• The polynomial-time hierarchy
• Type-based information flow analysis for the \(\pi\)-calculus
• Types as models: model checking message-passing programs
• Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the π-Calculus
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
• Well-structured transition systems everywhere!

Cited in

(3)

• Forward analysis for WSTS, part I: completions
• On hierarchical communication topologies in the \(\pi\)-calculus
• Deciding Safety Properties in Infinite-State Pi-Calculus via Behavioural Types

Describes a project that uses

Uses Software

• Petruchio
• SLMC
• PIPER

This page was built for publication: Deciding safety properties in infinite-state pi-calculus via behavioural types

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