diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java
new file mode 100644
index 0000000000..e3f574019c
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiAnalysis.java
@@ -0,0 +1,53 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+import hu.bme.mit.theta.analysis.InitFunc;
+import hu.bme.mit.theta.analysis.Prec;
+import hu.bme.mit.theta.analysis.expr.ExprState;
+import hu.bme.mit.theta.analysis.expr.StmtAction;
+
+import java.util.function.Function;
+
+public final class ExprMultiAnalysis<LState extends ExprState, RState extends ExprState, DataState extends ExprState, LBlank extends ExprState, RBlank extends ExprState,
+        LAction extends StmtAction, RAction extends StmtAction,
+        LPrec extends Prec, RPrec extends Prec, DataPrec extends Prec, LBlankPrec extends Prec, RBlankPrec extends Prec>
+        extends MultiAnalysis<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, ExprMultiState<LBlank, RBlank, DataState>, StmtMultiAction<LAction, RAction>> {
+
+    private ExprMultiAnalysis(Function<ExprMultiState<LBlank, RBlank, DataState>, MultiSourceSide> defineNextSide, Side<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide, Side<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide, InitFunc<DataState, DataPrec> dataInitFunc) {
+        super(defineNextSide, leftSide, rightSide, dataInitFunc);
+    }
+
+    public static <LState extends ExprState, RState extends ExprState, DataState extends ExprState, LBlank extends ExprState, RBlank extends ExprState,
+            LAction extends StmtAction, RAction extends StmtAction,
+            LPrec extends Prec, RPrec extends Prec, DataPrec extends Prec, LBlankPrec extends Prec, RBlankPrec extends Prec>
+    ExprMultiAnalysis<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec>
+    of(Side<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide, Side<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide,
+       Function<ExprMultiState<LBlank, RBlank, DataState>, MultiSourceSide> defineNextSide,
+       InitFunc<DataState, DataPrec> dataInitFunc) {
+        return new ExprMultiAnalysis<>(defineNextSide, leftSide, rightSide, dataInitFunc);
+    }
+
+    @Override
+    ExprMultiState<LBlank, RBlank, DataState> createInitialState(LBlank leftState, RBlank rightState, DataState dataState) {
+        return ExprMultiState.createInitial(leftState, rightState, dataState);
+    }
+
+    @Override
+    ExprMultiState<LBlank, RBlank, DataState> createState(LBlank leftState, RBlank rightState, DataState dataState, MultiSourceSide sourceSide) {
+        return ExprMultiState.create(leftState, rightState, dataState, sourceSide, true);
+    }
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java
new file mode 100644
index 0000000000..b6228dfe24
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiLts.java
@@ -0,0 +1,49 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+import hu.bme.mit.theta.analysis.LTS;
+import hu.bme.mit.theta.analysis.expr.ExprState;
+import hu.bme.mit.theta.analysis.expr.StmtAction;
+
+import java.util.function.BiFunction;
+import java.util.function.Function;
+
+public final class ExprMultiLts<LState extends ExprState, RState extends ExprState, DataState extends ExprState, LBlank extends ExprState, RBlank extends ExprState, LAction extends StmtAction, RAction extends StmtAction>
+        extends MultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction, ExprMultiState<LBlank, RBlank, DataState>, StmtMultiAction<LAction, RAction>> {
+
+    private ExprMultiLts(Function<ExprMultiState<LBlank, RBlank, DataState>, MultiSourceSide> defineNextSide, Side<LState, DataState, LBlank, LAction> left, Side<RState, DataState, RBlank, RAction> right) {
+        super(defineNextSide, left, right);
+    }
+
+    public static <LState extends ExprState, RState extends ExprState, DataState extends ExprState, LBlank extends ExprState, RBlank extends ExprState, LAction extends StmtAction, RAction extends StmtAction>
+    ExprMultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction> of(
+            LTS<? super LState, LAction> leftLts, BiFunction<LBlank, DataState, LState> wrapLeftState,
+            LTS<? super RState, RAction> rightLts, BiFunction<RBlank, DataState, RState> wrapRightState,
+            Function<ExprMultiState<LBlank, RBlank, DataState>, MultiSourceSide> defineNextSide) {
+        return new ExprMultiLts<>(defineNextSide, new Side<>(leftLts, wrapLeftState), new Side<>(rightLts, wrapRightState));
+    }
+
+    @Override
+    StmtMultiAction<LAction, RAction> wrapLeftAction(LAction action) {
+        return StmtMultiAction.ofLeftStmtAction(action);
+    }
+
+    @Override
+    StmtMultiAction<LAction, RAction> wrapRightAction(RAction action) {
+        return StmtMultiAction.ofRightStmtAction(action);
+    }
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiState.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiState.java
new file mode 100644
index 0000000000..86bb87be05
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/ExprMultiState.java
@@ -0,0 +1,50 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+import hu.bme.mit.theta.analysis.expr.ExprState;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And;
+
+public final class ExprMultiState<L extends ExprState, R extends ExprState, D extends ExprState> extends MultiState<L, R, D> implements ExprState {
+
+    private ExprMultiState(L ls, R rs, D data, MultiSourceSide sourceSide, boolean sourceMattersInEquality) {
+        super(ls, rs, data, sourceSide, sourceMattersInEquality);
+    }
+
+    public static <L extends ExprState, R extends ExprState, D extends ExprState> ExprMultiState<L, R, D> create(L ls, R rs, D d, MultiSourceSide sourceSide, boolean sourceMattersInEquality) {
+        return new ExprMultiState<>(ls, rs, d, sourceSide, sourceMattersInEquality);
+    }
+
+    public static <L extends ExprState, R extends ExprState, D extends ExprState> ExprMultiState<L, R, D> create(L ls, R rs, D d, MultiSourceSide sourceSide) {
+        return create(ls, rs, d, sourceSide, true);
+    }
+
+    public static <L extends ExprState, R extends ExprState, D extends ExprState> ExprMultiState<L, R, D> createInitial(L ls, R rs, D d, boolean sourceMattersInEquality) {
+        return create(ls, rs, d, null, sourceMattersInEquality);
+    }
+
+    public static <L extends ExprState, R extends ExprState, D extends ExprState> ExprMultiState<L, R, D> createInitial(L ls, R rs, D d) {
+        return createInitial(ls, rs, d, true);
+    }
+
+    @Override
+    public Expr<BoolType> toExpr() {
+        return And(And(getLeftState().toExpr(), getRightState().toExpr()), getDataState().toExpr());
+    }
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAction.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAction.java
new file mode 100644
index 0000000000..74d9c52188
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAction.java
@@ -0,0 +1,25 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+
+import hu.bme.mit.theta.analysis.Action;
+
+public interface MultiAction<L extends Action, R extends Action> extends Action {
+    L getLeftAction();
+
+    R getRightAction();
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysis.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysis.java
new file mode 100644
index 0000000000..2fb9277978
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysis.java
@@ -0,0 +1,120 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+import hu.bme.mit.theta.analysis.Action;
+import hu.bme.mit.theta.analysis.Analysis;
+import hu.bme.mit.theta.analysis.InitFunc;
+import hu.bme.mit.theta.analysis.PartialOrd;
+import hu.bme.mit.theta.analysis.Prec;
+import hu.bme.mit.theta.analysis.State;
+import hu.bme.mit.theta.analysis.TransFunc;
+
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.function.BiFunction;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
+
+/**
+ * @param <LState>    Type of combined (with data) state of left formalism
+ * @param <RState>    Type of combined (with data) state of right formalism
+ * @param <DataState> Type of data state
+ * @param <LBlank>    Type of blank state from left formalism
+ * @param <RBlank>    Type of blank state from right formalism
+ * @param <LAction>   Type of action from left formalism
+ * @param <RAction>   Type of action from right formalism
+ * @param <LPrec>     Type of precision of left formalism
+ * @param <RPrec>     Type of precision of right formalism
+ * @param <DataPrec>  Type of data precision (formalism independent)
+ */
+public abstract class MultiAnalysis<LState extends State, RState extends State, DataState extends State, LBlank extends State, RBlank extends State,
+        LAction extends Action, RAction extends Action,
+        LPrec extends Prec, RPrec extends Prec, DataPrec extends Prec, LBlankPrec extends Prec, RBlankPrec extends Prec,
+        MState extends MultiState<LBlank, RBlank, DataState>, MAction extends MultiAction<LAction, RAction>>
+        implements Analysis<MState, MAction, MultiPrec<LPrec, RPrec, DataPrec>> {
+
+    private final Function<MState, MultiSourceSide> defineNextSide;
+
+    private final Side<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide;
+    private final Side<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide;
+
+    private final InitFunc<DataState, DataPrec> dataInitFunc;
+
+    protected MultiAnalysis(Function<MState, MultiSourceSide> defineNextSide, Side<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide, Side<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide, InitFunc<DataState, DataPrec> dataInitFunc) {
+        this.defineNextSide = defineNextSide;
+        this.leftSide = leftSide;
+        this.rightSide = rightSide;
+        this.dataInitFunc = dataInitFunc;
+    }
+
+    abstract MState createInitialState(LBlank leftState, RBlank rightState, DataState dataState);
+
+    abstract MState createState(LBlank leftState, RBlank rightState, DataState dataState, MultiSourceSide sourceSide);
+
+    @Override
+    public PartialOrd<MState> getPartialOrd() {
+        return ((state1, state2) -> leftSide.analysis.getPartialOrd().isLeq(leftSide.combineStates.apply(state1.getLeftState(), state1.getDataState()), leftSide.combineStates.apply(state2.getLeftState(), state2.getDataState()))
+                && rightSide.analysis.getPartialOrd().isLeq(rightSide.combineStates.apply(state1.getRightState(), state1.getDataState()), rightSide.combineStates.apply(state2.getRightState(), state2.getDataState()))
+                && ((!state1.getSourceMattersInEquality() && !state2.getSourceMattersInEquality()) || (state1.getSourceSide() == state2.getSourceSide())));
+    }
+
+    @Override
+    public InitFunc<MState, MultiPrec<LPrec, RPrec, DataPrec>> getInitFunc() {
+        return (prec -> {
+            LBlankPrec leftInitPrec = leftSide.stripDataFromPrec.apply(prec.leftPrec());
+            RBlankPrec rightInitPrec = rightSide.stripDataFromPrec.apply(prec.rightPrec());
+            Collection<LBlank> leftInitStates = new HashSet<>(leftSide.initFunc.getInitStates(leftInitPrec));
+            Collection<RBlank> rightInitStates = new HashSet<>(rightSide.initFunc.getInitStates(rightInitPrec));
+            Collection<? extends DataState> dataInitStates = dataInitFunc.getInitStates(prec.dataPrec());
+            Collection<MState> resultSet = new HashSet<>();
+            for (LBlank leftInitState :
+                    leftInitStates) {
+                for (RBlank rightInitState :
+                        rightInitStates) {
+                    for (DataState dataInitState :
+                            dataInitStates) {
+                        resultSet.add(createInitialState(leftInitState, rightInitState, dataInitState));
+                    }
+                }
+            }
+            return resultSet;
+        });
+    }
+
+    @Override
+    public TransFunc<MState, MAction, MultiPrec<LPrec, RPrec, DataPrec>> getTransFunc() {
+        return ((state, action, prec) -> switch (defineNextSide.apply(state)) {
+            case LEFT -> {
+                final var succStates = leftSide.analysis.getTransFunc().getSuccStates(leftSide.combineStates().apply(state.getLeftState(), state.getDataState()), action.getLeftAction(), prec.leftPrec());
+                final Stream<MState> multiStateStream = succStates.stream().map(s -> createState(leftSide.stripDataFromState().apply(s), state.getRightState(), leftSide.extractDataFromState.apply(s), MultiSourceSide.LEFT));
+                yield multiStateStream.collect(Collectors.toSet());
+            }
+            case RIGHT -> {
+                final var succStates = rightSide.analysis.getTransFunc().getSuccStates(rightSide.combineStates.apply(state.getRightState(), state.getDataState()), action.getRightAction(), prec.rightPrec());
+                final Stream<MState> multiStateStream = succStates.stream().map(s -> createState(state.getLeftState(), rightSide.stripDataFromState.apply(s), rightSide.extractDataFromState.apply(s), MultiSourceSide.RIGHT));
+                yield multiStateStream.collect(Collectors.toSet());
+            }
+        });
+    }
+
+    public record Side<S extends State, DataS extends State, BlankS extends State, A extends Action, P extends Prec, BlankP extends Prec>
+            (Analysis<S, ? super A, ? super P> analysis, InitFunc<BlankS, BlankP> initFunc,
+             BiFunction<BlankS, DataS, S> combineStates, Function<S, BlankS> stripDataFromState,
+             Function<S, DataS> extractDataFromState, Function<P, BlankP> stripDataFromPrec) {
+    }
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysisBuilderFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysisBuilderFunc.java
new file mode 100644
index 0000000000..82c1f08ba8
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiAnalysisBuilderFunc.java
@@ -0,0 +1,37 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+import hu.bme.mit.theta.analysis.Action;
+import hu.bme.mit.theta.analysis.InitFunc;
+import hu.bme.mit.theta.analysis.Prec;
+import hu.bme.mit.theta.analysis.State;
+
+import java.util.function.Function;
+
+@FunctionalInterface
+public interface MultiAnalysisBuilderFunc<LState extends State, RState extends State, DataState extends State, LBlank extends State, RBlank extends State,
+        LAction extends Action, RAction extends Action,
+        LPrec extends Prec, RPrec extends Prec, DataPrec extends Prec, LBlankPrec extends Prec, RBlankPrec extends Prec,
+        MState extends MultiState<LBlank, RBlank, DataState>, MAction extends MultiAction<LAction, RAction>,
+        MAnalysis extends MultiAnalysis<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, MState, MAction>> {
+
+    MAnalysis build(MultiAnalysis.Side<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide,
+                    MultiAnalysis.Side<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide,
+                    Function<MState, MultiSourceSide> defineNextSide,
+                    InitFunc<DataState, DataPrec> dataInitFunc);
+
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiBuilder.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiBuilder.java
new file mode 100644
index 0000000000..7e5e6d1d16
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiBuilder.java
@@ -0,0 +1,95 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+import hu.bme.mit.theta.analysis.Action;
+import hu.bme.mit.theta.analysis.Analysis;
+import hu.bme.mit.theta.analysis.InitFunc;
+import hu.bme.mit.theta.analysis.LTS;
+import hu.bme.mit.theta.analysis.Prec;
+import hu.bme.mit.theta.analysis.State;
+
+import java.util.function.BiFunction;
+import java.util.function.Function;
+
+public final class MultiBuilder {
+
+    public static <LState extends State, LBlank extends State, LAction extends Action, DataState extends State, LPrec extends Prec, LBlankPrec extends Prec>
+    LeftSideAdded<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> initWithLeftSide(
+            Analysis<LState, ? super LAction, ? super LPrec> analysis, BiFunction<LBlank, DataState, LState> combineStates, Function<LState, LBlank> stripDataFromState, Function<LState, DataState> extractDataFromState, LTS<? super LState, LAction> lts, InitFunc<LBlank, LBlankPrec> initFunc, Function<LPrec, LBlankPrec> stripDataFromPrec
+    ) {
+        return new LeftSideAdded<>(analysis, combineStates, stripDataFromState, extractDataFromState, lts, initFunc, stripDataFromPrec);
+    }
+
+    public record Result<LState extends State, RState extends State, DataState extends State, LBlank extends State, RBlank extends State,
+            LAction extends Action, RAction extends Action,
+            LPrec extends Prec, RPrec extends Prec, DataPrec extends Prec, LBlankPrec extends Prec, RBlankPrec extends Prec,
+            MState extends MultiState<LBlank, RBlank, DataState>, MAction extends MultiAction<LAction, RAction>>
+            (MultiAnalysis<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, MState, MAction> analysis,
+             MultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction, MState, MAction> lts) {
+    }
+
+    public static class LeftSideAdded<LState extends State, DataState extends State, LBlank extends State, LAction extends Action, LPrec extends Prec, LBlankPrec extends Prec> {
+        private final MultiAnalysis.Side<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> side;
+        private final LTS<? super LState, LAction> lts;
+
+        LeftSideAdded(Analysis<LState, ? super LAction, ? super LPrec> analysis, BiFunction<LBlank, DataState, LState> combineStates, Function<LState, LBlank> stripDataFromState,
+                      Function<LState, DataState> extractDataFromState, LTS<? super LState, LAction> lts, InitFunc<LBlank, LBlankPrec> initFunc, Function<LPrec, LBlankPrec> stripDataFromPrec) {
+            this.lts = lts;
+            this.side = new MultiAnalysis.Side<>(analysis, initFunc, combineStates, stripDataFromState, extractDataFromState, stripDataFromPrec);
+        }
+
+        public <RState extends State, RBlank extends State, RAction extends Action, RPrec extends Prec, RBlankPrec extends Prec>
+        BothSidesDone<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, LBlankPrec, RBlankPrec>
+        addRightSide(Analysis<RState, ? super RAction, ? super RPrec> analysis, LTS<RState, RAction> rightLts,
+                     BiFunction<RBlank, DataState, RState> combineStates, Function<RState, RBlank> stripDataFromState, Function<RState, DataState> extractDataFromState,
+                     InitFunc<RBlank, RBlankPrec> initFunc, Function<RPrec, RBlankPrec> stripDataFromPrec) {
+            MultiAnalysis.Side<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide = new MultiAnalysis.Side<>(analysis, initFunc, combineStates, stripDataFromState, extractDataFromState, stripDataFromPrec);
+            return new BothSidesDone<>(side, lts, rightSide, rightLts);
+        }
+
+    }
+
+    public static class BothSidesDone<LState extends State, RState extends State, DataState extends State, LBlank extends State, RBlank extends State,
+            LAction extends Action, RAction extends Action,
+            LPrec extends Prec, RPrec extends Prec, LBlankPrec extends Prec, RBlankPrec extends Prec> {
+        private final MultiAnalysis.Side<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide;
+        private final LTS<? super LState, LAction> leftLts;
+        private final MultiAnalysis.Side<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide;
+        private final LTS<? super RState, RAction> rightLts;
+
+        BothSidesDone(MultiAnalysis.Side<LState, DataState, LBlank, LAction, LPrec, LBlankPrec> leftSide, LTS<? super LState, LAction> leftLts, MultiAnalysis.Side<RState, DataState, RBlank, RAction, RPrec, RBlankPrec> rightSide, LTS<? super RState, RAction> rightLts) {
+            this.leftSide = leftSide;
+            this.leftLts = leftLts;
+            this.rightSide = rightSide;
+            this.rightLts = rightLts;
+        }
+
+        public <DataPrec extends Prec, MState extends MultiState<LBlank, RBlank, DataState>, MAction extends MultiAction<LAction, RAction>>
+        Result<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, MState, MAction>
+        build(Function<MState, MultiSourceSide> defineNextSide, InitFunc<DataState, DataPrec> dataInitFunc,
+              MultiAnalysisBuilderFunc<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, MState, MAction,
+                      MultiAnalysis<LState, RState, DataState, LBlank, RBlank, LAction, RAction, LPrec, RPrec, DataPrec, LBlankPrec, RBlankPrec, MState, MAction>> analysisBuilderFunc,
+              MultiLtsBuilderFunc<LState, RState, DataState, LBlank, RBlank, LAction, RAction, MState, MAction, MultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction, MState, MAction>> ltsBuilderFunc) {
+            return new Result<>(
+                    analysisBuilderFunc.build(leftSide, rightSide, defineNextSide, dataInitFunc),
+                    ltsBuilderFunc.build(leftLts, leftSide.combineStates(), rightLts, rightSide.combineStates(), defineNextSide)
+            );
+        }
+
+    }
+
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLts.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLts.java
new file mode 100644
index 0000000000..de3354c9d0
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLts.java
@@ -0,0 +1,68 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+import hu.bme.mit.theta.analysis.Action;
+import hu.bme.mit.theta.analysis.LTS;
+import hu.bme.mit.theta.analysis.State;
+
+import java.util.Collection;
+import java.util.function.BiFunction;
+import java.util.function.Function;
+import java.util.stream.Stream;
+
+public abstract class MultiLts<LState extends State, RState extends State, DataState extends State, LBlank extends State, RBlank extends State, LAction extends Action, RAction extends Action, MState extends MultiState<LBlank, RBlank, DataState>, MAction extends MultiAction<LAction, RAction>>
+        implements LTS<MState, MAction> {
+
+    private final Function<MState, MultiSourceSide> defineNextSide;
+    private final Side<LState, DataState, LBlank, LAction> left;
+    private final Side<RState, DataState, RBlank, RAction> right;
+
+    protected MultiLts(Function<MState, MultiSourceSide> defineNextSide, Side<LState, DataState, LBlank, LAction> left, Side<RState, DataState, RBlank, RAction> right) {
+        this.defineNextSide = defineNextSide;
+        this.left = left;
+        this.right = right;
+    }
+
+    abstract MAction wrapLeftAction(LAction action);
+
+    abstract MAction wrapRightAction(RAction action);
+
+    @Override
+    public Collection<MAction> getEnabledActionsFor(MState state) {
+        return switch (defineNextSide.apply(state)) {
+            case LEFT -> {
+                Stream<LAction> actionStream = left.lts.getEnabledActionsFor(left.combineStates.apply(state.getLeftState(), state.getDataState())).stream();
+                Stream<MAction> multiActionStream = actionStream.map(this::wrapLeftAction);
+                yield multiActionStream.toList();
+            }
+            case RIGHT -> {
+                Stream<RAction> actionStream = right.lts.getEnabledActionsFor(right.combineStates.apply(state.getRightState(), state.getDataState())).stream();
+                Stream<MAction> multiActionStream = actionStream.map(this::wrapRightAction);
+                yield multiActionStream.toList();
+            }
+        };
+    }
+
+    public Function<MState, MultiSourceSide> getDefineNextSide() {
+        return defineNextSide;
+    }
+
+    protected record Side<S extends State, Data extends State, Blank extends State, A extends Action>(
+            LTS<? super S, A> lts, BiFunction<Blank, Data, S> combineStates) {
+    }
+
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLtsBuilderFunc.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLtsBuilderFunc.java
new file mode 100644
index 0000000000..b9153c6226
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiLtsBuilderFunc.java
@@ -0,0 +1,34 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+import hu.bme.mit.theta.analysis.Action;
+import hu.bme.mit.theta.analysis.LTS;
+import hu.bme.mit.theta.analysis.State;
+
+import java.util.function.BiFunction;
+import java.util.function.Function;
+
+@FunctionalInterface
+public interface MultiLtsBuilderFunc<LState extends State, RState extends State, DataState extends State, LBlank extends State, RBlank extends State,
+        LAction extends Action, RAction extends Action, MState extends MultiState<LBlank, RBlank, DataState>, MAction extends MultiAction<LAction, RAction>,
+        MLts extends MultiLts<LState, RState, DataState, LBlank, RBlank, LAction, RAction, MState, MAction>> {
+
+    MLts build(LTS<? super LState, LAction> leftLts, BiFunction<LBlank, DataState, LState> combineLeftState,
+               LTS<? super RState, RAction> rightLts, BiFunction<RBlank, DataState, RState> combineRightState,
+               Function<MState, MultiSourceSide> defineNextSide);
+
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiPrec.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiPrec.java
new file mode 100644
index 0000000000..b6a85ea69d
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiPrec.java
@@ -0,0 +1,37 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+import hu.bme.mit.theta.analysis.Prec;
+import hu.bme.mit.theta.core.decl.VarDecl;
+
+import java.util.Collection;
+
+public record MultiPrec<LPrec extends Prec, RPrec extends Prec, DataPrec extends Prec>(
+        LPrec leftPrec, RPrec rightPrec, DataPrec dataPrec) implements Prec {
+
+    @Override
+    public Collection<VarDecl<?>> getUsedVars() {
+        return dataPrec.getUsedVars();
+    }
+
+    @Override
+    public String toString() {
+        return "MultiPrec{" +
+                "dataPrec=" + dataPrec +
+                '}';
+    }
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiSourceSide.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiSourceSide.java
new file mode 100644
index 0000000000..dd4d8cd02e
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiSourceSide.java
@@ -0,0 +1,20 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+public enum MultiSourceSide {
+    LEFT, RIGHT
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiState.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiState.java
new file mode 100644
index 0000000000..72f65ad2ab
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/MultiState.java
@@ -0,0 +1,95 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+import com.google.common.base.Objects;
+import hu.bme.mit.theta.analysis.State;
+
+public abstract class MultiState<LState extends State, RState extends State, DataState extends State> implements State {
+
+    private final LState leftState;
+    private final RState rightState;
+    private final DataState dataState;
+
+    /**
+     * Denotes whether this state derived from an action that considered the left state of the previous multi state.
+     * Can be null. Is always null for initial states.
+     */
+    private final MultiSourceSide sourceSide;
+
+    /**
+     * Flag whether to include {@link hu.bme.mit.theta.analysis.multi.MultiState#sourceSide} in {@link hu.bme.mit.theta.analysis.multi.MultiState#equals(Object)}
+     */
+    private final boolean sourceMattersInEquality;
+
+    protected MultiState(LState ls, RState rs, DataState data, MultiSourceSide sourceSide, boolean sourceMattersInEquality) {
+        leftState = ls;
+        rightState = rs;
+        dataState = data;
+        this.sourceSide = sourceSide;
+        this.sourceMattersInEquality = sourceMattersInEquality;
+    }
+
+    public MultiSourceSide getSourceSide() {
+        return sourceSide;
+    }
+
+    @Override
+    public boolean isBottom() {
+        return dataState.isBottom() || leftState.isBottom() || rightState.isBottom();
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (this == o) return true;
+        if (o == null || getClass() != o.getClass()) return false;
+        MultiState<?, ?, ?> that = (MultiState<?, ?, ?>) o;
+        if ((sourceMattersInEquality || that.sourceMattersInEquality) && sourceSide != that.sourceSide)
+            return false;
+        return Objects.equal(leftState, that.leftState) && Objects.equal(rightState, that.rightState) && Objects.equal(dataState, that.dataState);
+    }
+
+    @Override
+    public int hashCode() {
+        return Objects.hashCode(leftState, rightState, dataState, sourceSide, sourceMattersInEquality);
+    }
+
+
+    public LState getLeftState() {
+        return leftState;
+    }
+
+    public RState getRightState() {
+        return rightState;
+    }
+
+    public DataState getDataState() {
+        return dataState;
+    }
+
+    public boolean getSourceMattersInEquality() {
+        return sourceMattersInEquality;
+    }
+
+    @Override
+    public String toString() {
+        return "MultiState{" +
+                "leftState=" + leftState +
+                ", rightState=" + rightState +
+                ", dataState=" + dataState +
+                '}';
+    }
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/RefToMultiPrec.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/RefToMultiPrec.java
new file mode 100644
index 0000000000..c913f6374e
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/RefToMultiPrec.java
@@ -0,0 +1,38 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+import hu.bme.mit.theta.analysis.Prec;
+import hu.bme.mit.theta.analysis.expr.refinement.Refutation;
+import hu.bme.mit.theta.analysis.expr.refinement.RefutationToPrec;
+
+public record RefToMultiPrec<LPrec extends Prec, RPrec extends Prec, DataPrec extends Prec, R extends Refutation>(
+        RefutationToPrec<LPrec, R> leftRefToPrec,
+        RefutationToPrec<RPrec, R> rightRefToPrec,
+        RefutationToPrec<DataPrec, R> dataRefToPrec
+)
+        implements RefutationToPrec<MultiPrec<LPrec, RPrec, DataPrec>, R> {
+
+    @Override
+    public MultiPrec<LPrec, RPrec, DataPrec> toPrec(R refutation, int index) {
+        return new MultiPrec<>(leftRefToPrec.toPrec(refutation, index), rightRefToPrec().toPrec(refutation, index), dataRefToPrec().toPrec(refutation, index));
+    }
+
+    @Override
+    public MultiPrec<LPrec, RPrec, DataPrec> join(MultiPrec<LPrec, RPrec, DataPrec> prec1, MultiPrec<LPrec, RPrec, DataPrec> prec2) {
+        return new MultiPrec<>(leftRefToPrec.join(prec1.leftPrec(), prec2.leftPrec()), rightRefToPrec.join(prec1.rightPrec(), prec2.rightPrec()), dataRefToPrec.join(prec1.dataPrec(), prec2.dataPrec()));
+    }
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/StmtMultiAction.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/StmtMultiAction.java
new file mode 100644
index 0000000000..f781e4633d
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/multi/StmtMultiAction.java
@@ -0,0 +1,66 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.multi;
+
+import hu.bme.mit.theta.analysis.expr.StmtAction;
+import hu.bme.mit.theta.core.stmt.Stmt;
+
+import java.util.List;
+
+public final class StmtMultiAction<L extends StmtAction, R extends StmtAction> extends StmtAction implements MultiAction<L, R> {
+    private final L leftAction;
+    private final R rightAction;
+
+    private StmtMultiAction(L lAction, R rAction) {
+        leftAction = lAction;
+        rightAction = rAction;
+    }
+
+    public static <L extends StmtAction, R extends StmtAction> StmtMultiAction<L, R> ofLeftStmtAction(L action) {
+        return new StmtMultiAction<>(action, null);
+    }
+
+    public static <L extends StmtAction, R extends StmtAction> StmtMultiAction<L, R> ofRightStmtAction(R action) {
+        return new StmtMultiAction<>(null, action);
+    }
+
+    public StmtAction getAction() {
+        return getLeftAction() == null ? getRightAction() : getLeftAction();
+    }
+
+    @Override
+    public String toString() {
+        return "ExprMultiAction{" +
+                "leftAction=" + leftAction +
+                ", rightAction=" + rightAction +
+                '}';
+    }
+
+    @Override
+    public List<Stmt> getStmts() {
+        return getAction().getStmts();
+    }
+
+    @Override
+    public L getLeftAction() {
+        return leftAction;
+    }
+
+    @Override
+    public R getRightAction() {
+        return rightAction;
+    }
+}