Valid formulas, games and network protocols
Jean-Louis Krivine (PPS), Yves Legrandg\'erard (PPS)
TL;DR
This paper explores the connection between valid formulas in predicate logic and the specification of network protocols, providing examples and methods for protocol composition.
Contribution
It introduces a novel approach linking logical validity with network protocol specification and demonstrates how to specify protocol composition.
Findings
Logical validity corresponds to protocol correctness
Examples include packet acknowledgment protocols
Method for specifying protocol composition
Abstract
We describe a remarkable relation between the notion of valid formula of predicate logic and the specification of network protocols. We give several examples such as the acknowledgement of one packet or of a sequence of packets. We show how to specify the composition of protocols.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, Reasoning, and Knowledge · Logic, programming, and type systems