2012/03/06 by Tichakorn Wongpiromsarn, Wongpiromsarn, Tichakorn, Alphan Ulusoy +8
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Robotics (cs.RO) #cs.RO
paper · pdf · doi:10.48550/arxiv.1203.1180
arxiv created 2012/03/06 · openalex publication_date 2012/03/06 · arxiv updated 2012/03/07 · openalex created_date 2025/10/24 · openalex updated_date 2026/07/28
We consider the synthesis of control policies from temporal logic specifications for robots that interact with multiple dynamic environment agents. Each environment agent is modeled by a Markov chain whereas the robot is modeled by a finite transition system (in the deterministic case) or Markov decision process (in the stochastic case). Existing results in probabilistic verification are adapted to solve the synthesis problem. To partially address the state explosion issue, we propose an incremental approach where only a small subset of environment agents is incorporated in the synthesis procedure initially and more agents are successively added until we hit the constraints on computational resources. Our algorithm runs in an anytime fashion where the probability that the robot satisfies its specification increases as the algorithm progresses.