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

DOI10.1016/j.ic.2012.01.006zbMath1279.68192OpenAlexW1984379137MaRDI QIDQ418155

Michele Boreale, Lucia Acciai

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

safetydecidabilitypi-calculusbehavioural typesspatial logic

Mathematics Subject Classification ID

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

Related Items

Forward analysis for WSTS, part I: completions

Uses Software

• Petruchio
• SLMC
• PIPER

Cites Work

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