MultiAgentGamePlay/LTL_Formulation.html at main · wfishell/MultiAgentGamePlay · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
<!DOCTYPE html>
<html lang="en">
<head>
  <meta charset="UTF-8">
  <title>LLM to LTL formulation Pipeline</title>
  <style>
    body {
      font-family: Arial, sans-serif;
      margin: 20px;
    }
    .container {
      display: flex;
      flex-direction: column;
      gap: 20px;
    }
    pre {
      background-color: #f4f4f4;
      padding: 15px;
      border-radius: 5px;
      overflow-x: auto;
      white-space: pre-wrap; /* Enables text wrapping */
      word-wrap: break-word;
    }
    .image-block img {
      width: 100%; /* Makes the image larger by taking full container width */
      max-width: 800px; /* Limits maximum size for larger displays */
      height: auto;
      border: 1px solid #ccc;
      border-radius: 5px;
      display: block;
      margin: 0 auto;
    }
    .image-block h2 {
      text-align: center;
      margin-bottom: 10px;
    }
    .image-block figcaption {
      text-align: center;
      font-style: italic;
      margin-top: 5px;
    }
  </style>
</head>
<body>
  <h1>LLM to LTL formulation Pipeline</h1>

  <p>
    We pass in text descriptions of our games, with a high level description of the gameplay, system requirements, and liveness requirements. Using this information, the LLM outputs a JSON file with LTL formulation, system Player information, and environment player information. We then construct a parity game to check this LTL specification is realizable. If it is not, regenerate the LTL specification; otherwise, we continue to generate the game.
  </p>

  <div class="container">
    <pre>{
  "ltl_formulation": "G(safe_robots & safe_moves & correct_state_changes & obstacle_avoidance & continuous_movement & package_delivery & adaptive_routing & zone_clearing) & GF(new_packages)",
  "System_Player": {
    "name": "Robots",
    "init": "All robots start in the navigating state at their initial positions",
    "safety": "Robots never share a grid cell, avoid static obstacles (cell walls and delivered packages), avoid dynamic obstacles (other robots and undelivered boxes), carry at most one package at a time, ensure delivered packages don't block critical pathways to delivery zones, change states only when properly positioned (pickups at spawn points, drop-offs in delivery zones)",
    "prog": "Robots must move to a new legal grid cell at each time step, must eventually pick up and deliver assigned packages, must continuously adapt routes as obstacles change, once all packages for a time step are delivered, boxes in the delivery zone are removed"
  },
  "Environment_Player": {
    "name": "Warehouse",
    "init": "Initial grid configuration with static obstacles (cell walls) and package spawn points",
    "safety": "New packages are generated only after all current packages are delivered, at most four packages per robot zone at any time",
    "prog": "Intermittently generate new packages at specific time steps"
  },
  "Inputs": [
    "Robot positions",
    "Robot states",
    "Grid configuration (obstacles and package locations)"
  ],
  "Outputs": [
    "Robot positions",
    "Robot states",
    "Grid configuration (obstacles and package locations)"
  ]
}</pre>

    <div class="image-block">
      <h2>LLM to LTL Pipeline</h2>
      <figure>
        <img src="LLM_LTL_Pipeline.png" alt="LLM to LTL pipeline">
      </figure>
    </div>
  </div>
</body>
</html>