diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/README.md b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/README.md
new file mode 100644
index 0000000000..91de66f36c
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/README.md
@@ -0,0 +1,13 @@
+## Overview
+
+This package contains two new data structures, a Proof and a Cex.
+
+### Abstract State Graph
+
+`ASG` is a more simple state space representation than `ARG`. It works and is implemented in a very similar way,
+except it does allow circles to appear in the graph.
+
+### ASG trace
+
+`ASGTrace` represents a lasso like trace, i.e. it is made with two parts: a tail and a loop. The loop is required
+to start and end in the last state of the tail. This node in the graph is called honda.
\ No newline at end of file
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/README.md b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/README.md
new file mode 100644
index 0000000000..bd08f4b484
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/README.md
@@ -0,0 +1,88 @@
+## Overview
+
+This package provides algorithms that allow to look for accepting lasso shaped traces in a state space.
+A lasso is a special form of trace, consisting of two parts: a tail and a loop. Both are like classic traces, where the
+tail has to start from an initial state, and the loop has to start and end in the last state of the tail.
+Loopchecker has to be provided with a predicate that can mark either states or actions as accepting. The loop checking
+algorithms look for lasso traces that have such acceptance in their loop.
+
+## Data structures
+
+The data structures in Theta had a limitation that made them not suitable for the initial implementation of loopchecker.
+Both ARG and Trace do not allow circles to appear in the state space. For this reason, loopchecker uses the
+`hu.bme.mit.theta.analysis.algorithm.asg` package.
+
+## Algorithms
+For abstraction and trace concretization there are 2-2 algorithms, completely interchangeable. This is implemented
+using the strategy design pattern.
+
+### Abstraction
+
+During abstraction, the `ASG` is built and explored until a valid `ASGTrace` is found. There are currently two algorithms
+implemented, both based on a dept first search.
+
+#### Nested Depth-First Search
+
+NDFS contains of two Depth-First searches right after eachother to find a lasso trace. The goal of the first DFS
+is to find any acceptance, and than the second should find the very same acceptance from there.
+
+![]()
+
+
+#### Guided depth first search
+
+The basis of the
+algorithm is Depth-First Search (DFS), where we do only one search with a modified
+condition instead of two nested ones compared to NDFS. Let us call encountering an accepting state/transition an acceptance. In the DFS, while keeping an acceptance counter,
+look for a node that is already on the stack and has a smaller value on the counter
+than the top of the stack.
+
+![]()
+
+
+### Concretization
+
+Concretizing a lasso trace requires an extra step after simple concretization. First the lasso is straightened to a classic
+trace, and a classic concretization is used to determine if it's even feasible. However, after that, one needs to make
+sure that the loop of the lasso is also a possible loop in the concrete state space.
+
+#### Milano
+
+This is a more direct approach. It checks whether the honda can be in the same
+state before and after the loop. This is done by adding the cycle validity constraint to the
+loop. An expression is added to the solver that requires all variables to have the same value in the first and
+last state of the loop.
+
+![]()
+
+#### Bounded unrolling
+
+The idea of bounded unwinding comes from E. Clarke et al., who defined an algorithm
+to detect and refine lasso-shaped traces in the abstract state-space. The idea was that
+even though we do not know if an abstract loop directly corresponds to a concrete loop,
+we can be sure that the abstract loop can be concretized at most m different ways, where
+m is the size of the smallest abstract state in the loop (if we think about abstract states as
+sets of concrete states). That is because, if the loop is run m times and is concretizable,
+the state that had the smallest number of concrete states has to repeat itself at least once.
+The only limitations of the original algorithm were that it was defined for deterministic
+operations only.
+
+To slightly mitigate this limitation and be able to use the algorithm, we need to eliminate as many nondeterministic operations as possible. To achieve this, nondeterministic
+operations have to be unfolded: they are replaced with all their possible deterministic
+counterparts. For the nondet operations of `xsts`, this can be seen in the `XstsNormalizerPass` pass object.
+
+Another limitation of the original algorithm in our context is that Theta is working with
+possibly infinite domains, for which m could also potentially evaluate to infinite. To have a
+chance to avoid these infinite unwindings, it is worth noting that counting all the concrete
+states allowed by the abstract states in the loop is an overapproximation of the number
+of all possible different states the concrete loop can reach. If a variable is included in only
+such assignments (or no assignments at all) where the expression contains only literals,
+that variable has a fixed value throughout the loop. That means, for such variables, just
+one unwinding is enough.
+
+To find all the variables that contribute towards the needed number of unwindings, `VarCollectorStatementVisitor` is used.
+![]()
+
+Since infinite bounds can
+still be encountered, there is a configurable maximum for the bound. If m would be greater
+than that, the refiner falls back to the default concretizer algorithm, which is Milano in the current implementation.
diff --git a/subprojects/common/ltl-cli/README.md b/subprojects/common/ltl-cli/README.md
new file mode 100644
index 0000000000..f839575586
--- /dev/null
+++ b/subprojects/common/ltl-cli/README.md
@@ -0,0 +1,4 @@
+## Overview
+This package contains classes and objects related to CLIs that allow LTL model checking. For now it only contains a helper class
+that is an implementation of the Clikt's package OptionGroup. This option group allows the user to select from the available
+loopchecker and loop refinement strategies.
\ No newline at end of file
diff --git a/subprojects/common/ltl/doc/README.md b/subprojects/common/ltl/doc/README.md
new file mode 100644
index 0000000000..bf0078de64
--- /dev/null
+++ b/subprojects/common/ltl/doc/README.md
@@ -0,0 +1,76 @@
+## Overview
+This project has two main purposes. The `hu.bme.mit.theta.common.cfa.buchi` package is used to convert properties specified
+in the LTL language to Buchi automata as CFA. The `hu.bme.mit.theta.common.ltl` package contains a SafetyChecker that
+is able to perform LTL based model checking on any formalism.
+
+## Converting LTL to Buchi automaton
+
+The main job is done by implementations of the `Ltl2BuchiTransformer` interface. This accepts an LTL formula and
+produces a Buchi automaton in Theta representation. The current implementation `Ltl2BuchiThroughHoaf` does the following:
+
+1. Preprocess the input LTL expression by substituting complex expressions with atomic propositions
+2. Call a `Ltl2Hoaf` converter that produces the Buchi automaton in the [Hanoi Omega-Automata Format](https://adl.github.io/hoaf/)
+3. Use the `BuchiBuilder` object to read the HOAF string and generate a CFA
+
+
+
+### Preprocessing
+Linear Temporal Logic works with atomic propositions, i.e. variables and expressions can only be of type boolean.
+In align to this, most tools won't accept complex formulae, like `F(x == 9)`, i.e. _x is eventually going to become 9_.
+To support such expressions, a preprocessing step is implemented. The entry point is in the `ToStringVisitor` class.
+This class creates a new, now valid LTL expression with only atomic propositions, and provides a mapping from these
+propositions to the original expressions. In our previoues example, the result could be `F p0`, and the mapping would contain
+`p0 -> x == 9`.
+
+### The purpose of [Hanoi Omega-Automata Format](https://adl.github.io/hoaf/) in the implementation
+Since there were no tools or libraries that could have been linked due to licensing issues, it was required
+to support calling external tools. HOAF is a standard that has many advantages for us:
+
+* It's widely accepted and adopted by most of the tools related to LTL manipulation
+* It's a rather stable but still maintained standard
+* There is a library which is now included with theta that provides interfaces to work with HOAF
+
+This allows the end-user to use any tool for the conversion they'd like. They only need to provided a command that runs on their system
+and when the `ExternalLtl2Hoaf` runs it by appending the processed LTL formula after it, returns a Buchi automaton in the HOA format.
+
+The recommended tools are [Spot](https://spot.lre.epita.fr/) and [Owl](https://owl.model.in.tum.de/).
+
+
+### Why CFA?
+
+Implementing Buchi automaton from scratch would have resulted in a lot of duplicate code with the already existing CFA class.
+For this reason, CFA is now extended with optional accepting states or edges. Such CFA can perfectly model a Buchi automaton.
+
+Of course, it would be more desirable, to have a common automaton superclass for CFA and a new Buchi automaton, but this was
+not in scope for the project that developed these packages.
+
+### Automated testing of LTL checking
+
+Running external tools during automated testing such as in the CI/CD processes is not that feasible in the case of Theta.
+For various reasons, our tests run on many different platforms. Running the above recommended programs during these tests
+would result in a maintenance nightmare:
+
+* The tools would need to be installed on all runner images
+* Since most of them are only distributed for linux, calling them would require to be different on different operating systems
+ * For example, on windows you might use `WSL`, but the command `wsl` would of course fail on a linux system
+
+For this reason, testing is done with another implementation of `Ltl2Hoaf`. `Ltl2HoafFromDir` is a class that expects
+a directory as a parameter. Than when called with an LTL formula, encodes the formula to URL and looks up the resulting
+filename.hoa in the directory.
+
+### Architecture
+
+The above interfaces and objects form the following architecture:
+
+
+
+## LTL checking
+
+In the ltl package there is a single class the `LtlChecker`. This is a subclass of the safety checker, so it can fit
+into most CLI algorithms easily. It uses the conversion mechanisms to create a Buchi automaton. Then uses the
+`hu.bme.mit.theta.analysis.multi` package to create a product of this buchi automaton and the model that needs to
+be checket. Finally it simply constructs a loopchecker abstractor and refiner, than builds
+a `CegarChecker` with them.
+
+For the details of the model checking algorithms, look at the `hu.bme.mit.theta.analysis.algorithm.loopchecker` package
+in the common analysis subproject.
\ No newline at end of file
diff --git a/subprojects/common/ltl/doc/ltl2buchi.drawio b/subprojects/common/ltl/doc/ltl2buchi.drawio
new file mode 100644
index 0000000000..27f8690cb9
--- /dev/null
+++ b/subprojects/common/ltl/doc/ltl2buchi.drawio
@@ -0,0 +1,70 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/subprojects/common/ltl/doc/ltl2buchi.jpg b/subprojects/common/ltl/doc/ltl2buchi.jpg
new file mode 100644
index 0000000000..f58d526a38
Binary files /dev/null and b/subprojects/common/ltl/doc/ltl2buchi.jpg differ
diff --git a/subprojects/common/ltl/doc/ltl_conversion_pipeline.drawio b/subprojects/common/ltl/doc/ltl_conversion_pipeline.drawio
new file mode 100644
index 0000000000..a908f9a612
--- /dev/null
+++ b/subprojects/common/ltl/doc/ltl_conversion_pipeline.drawio
@@ -0,0 +1,31 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/subprojects/common/ltl/doc/ltl_conversion_pipeline.jpg b/subprojects/common/ltl/doc/ltl_conversion_pipeline.jpg
new file mode 100644
index 0000000000..b36fa27f40
Binary files /dev/null and b/subprojects/common/ltl/doc/ltl_conversion_pipeline.jpg differ
diff --git a/subprojects/xsts/xsts-cli/README.md b/subprojects/xsts/xsts-cli/README.md
index 0054a2175d..32ec44206f 100644
--- a/subprojects/xsts/xsts-cli/README.md
+++ b/subprojects/xsts/xsts-cli/README.md
@@ -28,12 +28,13 @@ the [`xsts`](../xsts/README.md) project.
2. Running the tool requires Java (JRE) 17.
3. The tool also requires the [Z3 SMT solver libraries](../../../doc/Build.md) to be available
on `PATH`.
-4. The tool can be executed with `java -jar theta-xsts-cli.jar [ARGUMENTS]`.
+4. The tool can be executed with `java -jar theta-xsts-cli.jar [SUBCOMMAND] [ARGUMENTS]`.
+ * SUBCOMMAND should be the algorithm you want to run (Previous commands with the `--algorithm` switch should move the value here)
* If no arguments are given, a help screen is displayed about the arguments and their possible
values.
More information can also be found below.
* For
- example `java -jar theta-xsts-cli.jar --model crossroad.xsts --property "x>1" --loglevel INFO`
+ example `java -jar theta-xsts-cli.jar CEGAR --model crossroad.xsts --property "x>1" --loglevel INFO`
runs the default analysis with logging on the `crossroad.xsts` model file with the
property `x>1`.
@@ -55,40 +56,48 @@ residing on the host:
Note that the model must be given as the first positional argument (without `--model`).
-## Arguments
-
-All arguments are optional, except `--model` and `--property`.
-
-* `--model`: Path of the input XSTS model (mandatory). Can also accept PNML files with the `*.pnml`
- extension.
-* `--property`: Input property as a string or a file (*.prop) (mandatory). For PNML models an unsafe
- target marking can also be described by listing the values of each place in their order of
- definition separated with spaces.
-* `--cex`: Output file where the counterexample is written (if the result is unsafe). If the
- argument is not given (default) the counterexample is not printed. Use `CON` (Windows)
- or `/dev/stdout` (Linux) as argument to print to the standard output.
-* `--loglevel`: Detailedness of logging.
- * Possible values (from the least to the most detailed): `RESULT`, `MAINSTEP`, `SUBSTEP` (
- default), `INFO`, `DETAIL`, `VERBOSE`.
-* `--version`: Print version info (in this case `--model` and `--property` is of course not
- required).
-* `--metrics`: Print metrics about the XSTS model (number of variables and statements).
-* `--initialmarking`: Can be used with the PNML frontend. Override the initial markings of the
- places. Format: list the values to be assigned to each place in the order of their definition in
- the PNML file separated with spaces.
-* `--visualize`: Visualize the result of the analysis (the reachability graph if the model is safe,
- or a counterexample trace if it is unsafe). Prints to the dotfile given as parameter.
-* `--optimizestmts`: The algorithm can optimize stmts by detecting failing assumptions and
- unreachable branches of choices.
- * Possible values: `ON` (default), `OFF`.
-
-The arguments related to the algorithm are described in more detail (along with best practices)
-in [CEGAR-algorithms.md](../../../doc/CEGAR-algorithms.md).
-
-### For developer usage
-
-| Flag | Description |
-|----------------|-----------------------------------------------------|
-| `--stacktrace` | Print full stack trace for exceptions. |
-| `--benchmark` | Benchmark mode, only print metrics in csv format. |
-| `--header` | Print the header for the benchmark mode csv format. |
+## Subcommands
+There are two categories of subcommands, one for model checking and one for helper texts. For up to date information, run the
+CLI without any subcommand, or with the `--help` flag and the available subcommands will be printed for you.
+### Algorithms
+The following subcommands are available as arguments:
+
+| **Feature** | **Description** |
+|---------------------|----------------------------------------------------------------------------------------------------------------------------------|
+| **CEGAR** | Model checking using the CEGAR (CounterExample Guided Abstraction Refinement) algorithm |
+| **LTLCEGAR** | Model checking using the CEGAR algorithm with an LTL property |
+| **BOUNDED** | Bounded model checking algorithms (BMC, IMC, KINDUCTION). Use `--variant` to select the algorithm (by default, BMC is selected). |
+| **MDD** | Model checking of XSTS using MDDs (Multi-value Decision Diagrams) |
+| **PN_MDD** | Model checking of Petri nets using MDDs (Multi-value Decision Diagrams) |
+| **CHC** | Model checking using the Horn solving backend |
+
+### Helper commands
+There are two subcommands that simply output information:
+
+* **header** : Used to print a header for outputs generated by the `--benchmark` option in the algorithm commands. If you are doing
+a larger benchmark with multiple runs piping into a file, this can be run first to provide a header for the file
+* **metrics** : Prints information about the input xsts model
+
+## Common arguments
+
+There is two group of arguments that are mostly common among all the algorithm subcommands.
+
+### Input options
+Options related to model and property input
+
+| **Option** | **Description** |
+|----------------------------|-------------------------------------------------------------------------------------------------------------|
+| `--model=` | Path of the input model (XSTS or Pnml). Extension should be `.pnml` to be handled as Petri-net input |
+| `--property=` | Path of the property file. Has priority over `--inlineProperty` |
+| `--inline-property=` | Input property as a string. Ignored if `--property` is defined |
+
+### Output options
+Options related to output and statistics
+
+| **Option** | **Description** |
+|------------------------|--------------------------------------------------------------------------------------------------------|
+| `--log-level=` | Detailedness of logging. Possible values: `RESULT`, `MAINSTEP`, `SUBSTEP`, `INFO`, `DETAIL`, `VERBOSE` |
+| `--benchmark=` | Quiet mode, output will be just the result metrics. Possible values: `true`, `false` |
+| `--cexfile=` | Write concrete counterexample to a file |
+| `--stacktrace` | Print stack trace of exceptions |
+| `--visualize=` | Write proof or counterexample to file in DOT format |