Towards Probabilistic Strategic Timed CTL
Wojciech Jamroga, Marta Kwiatkowska, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
TL;DR
This paper introduces PSTCTL, a probabilistic extension of Strategic Timed CTL, enabling the verification of stochastic multi-agent systems with continuous time and strategic considerations.
Contribution
It defines PSTCTL, a new probabilistic logic for strategic reasoning in stochastic timed systems, and demonstrates the feasibility of verification using irP-strategies.
Findings
PSTCTL effectively models probabilistic strategic properties.
Verification with irP-strategies is feasible for PSTCTL.
Provides a foundation for probabilistic strategic system analysis.
Abstract
We define PSTCTL, a probabilistic variant of Strategic Timed CTL (STCTL), interpreted over stochastic multi-agent systems with continuous time and asynchronous execution semantics. STCTL extends TCTL with strategic operators in the style of ATL. Moreover, we demonstrate the feasibility of verification with irP-strategies.
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 · Multi-Agent Systems and Negotiation