Formula Synthesis in Propositional Dynamic Logic with Shuffle
Authors: Sophie Pinchinat, Sasha Rubin, François Schwarzentruber9902-9909
AAAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We prove that the problem is undecidable in general, but add certain restrictions on the input structure or on the input grammar to yield decidability. In particular, we prove that (1) if the grammar only generates formulas in PDL (without shuffle), then the problem is EXPTIME-complete, and a further restriction to linear grammars is PSPACE-complete, and a further restriction to non-recursive grammars is NP-complete, and (2) if one restricts the input structure to have only simple paths then the problem is in 2-EXPTIME. |
| Researcher Affiliation | Academia | Sophie Pinchinat1, Sasha Rubin2, Franc ois Schwarzentruber1 1IRISA/Univ Rennes, France 2The university of Sydney, Australia sophie.pinchinat@irisa.fr, sasha.rubin@sydney.edu.au, francois.schwarzentruber@ens-rennes.fr |
| Pseudocode | No | The paper describes algorithmic procedures in natural language but does not include any formal pseudocode or algorithm blocks. |
| Open Source Code | No | The paper is theoretical and does not mention releasing source code or provide any links for it. |
| Open Datasets | No | This is a theoretical paper and does not involve the use of datasets for training or evaluation. |
| Dataset Splits | No | This is a theoretical paper and does not involve data splits for training, validation, or testing. |
| Hardware Specification | No | This is a theoretical paper and does not describe any experimental setup requiring hardware specifications. |
| Software Dependencies | No | This is a theoretical paper and does not mention specific software dependencies with version numbers. |
| Experiment Setup | No | This is a theoretical paper and does not describe any experimental setup details such as hyperparameters or training configurations. |