International Center for Computational Logic - Benutzerbeiträge [de]

Inproceedings2598778905

2026-08-25T12:12:27Z

Rajab Aghamov:

{{Publikation Erster Autor
|ErsterAutorVorname=Rajab
|ErsterAutorNachname=Aghamov
|FurtherAuthors=Christel Baier; Toghrul Karimov; Joël Ouaknine; Jakob Piribauer
}}
{{Inproceedings
|Referiert=0
|Title=Linear dynamical systems with continuous weight functions
|To appear=0
|Year=2024
|Booktitle=Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024, Hong Kong SAR, China, May 14-16, 2024
|Pages=22:1--22:11
|Publisher=ACM
|Editor=Erika Ábrahám and Manuel Mazo Jr.
}}
{{Publikation Details
|Bild=Logo-2 (1) (1).jpg
|Abstract=In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight function assigning weights to the points in the orbit can be used to model quantitative aspects, such as resource consumption, of a system modelled by an LDS. This paper addresses the problems to compute the mean payoff, the total accumulated weight, and the discounted accumulated weight of the orbit under continuous weight functions and polynomial weight functions as a special case. Besides general LDSs, the special cases of stochastic LDSs and of LDSs with bounded orbits are considered. Furthermore, the problem of deciding whether an energy constraint is satisfied by the weighted orbit, i.e., whether the accumulated weight never drops below a given bound, is analysed.
|DOI Name=10.1145/3641513.3650173
|Projekt=CPEC, SECAI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Inproceedings2598778905

2026-08-25T12:11:48Z

Rajab Aghamov:

{{Publikation Erster Autor
|ErsterAutorVorname=Rajab
|ErsterAutorNachname=Aghamov
|FurtherAuthors=Christel Baier; Toghrul Karimov; Joël Ouaknine; Jakob Piribauer
}}
{{Inproceedings
|Referiert=0
|Title=Linear dynamical systems with continuous weight functions
|To appear=0
|Year=2024
|Booktitle=Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024, Hong Kong SAR, China, May 14-16, 2024
|Pages=22:1--22:11
|Publisher=ACM
|Editor=Erika Ábrahám and Manuel Mazo Jr.
}}
{{Publikation Details
|Bild=Logo-2 (1) (1).jpg
|Abstract=In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight function assigning weights to the points in the orbit can be used to model quantitative aspects, such as resource consumption, of a system modelled by an LDS. This paper addresses the problems to compute the mean payoff, the total accumulated weight, and the discounted accumulated weight of the orbit under continuous weight functions and polynomial weight functions as a special case. Besides general LDSs, the special cases of stochastic LDSs and of LDSs with bounded orbits are considered. Furthermore, the problem of deciding whether an energy constraint is satisfied by the weighted orbit, i.e., whether the accumulated weight never drops below a given bound, is analysed.
|DOI Name=10.1145/3641513.3650173
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Datei:Logo-2 (1) (1).jpg

2026-08-25T12:11:45Z

Rajab Aghamov:

Inproceedings2598778905

2026-08-25T12:11:25Z

Rajab Aghamov:

{{Publikation Erster Autor
|ErsterAutorVorname=Rajab
|ErsterAutorNachname=Aghamov
|FurtherAuthors=Christel Baier; Toghrul Karimov; Joël Ouaknine; Jakob Piribauer
}}
{{Inproceedings
|Referiert=0
|Title=Linear dynamical systems with continuous weight functions
|To appear=0
|Year=2024
|Booktitle=Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024, Hong Kong SAR, China, May 14-16, 2024
|Pages=22:1--22:11
|Publisher=ACM
|Editor=Erika Ábrahám and Manuel Mazo Jr.
}}
{{Publikation Details
|Abstract=In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight function assigning weights to the points in the orbit can be used to model quantitative aspects, such as resource consumption, of a system modelled by an LDS. This paper addresses the problems to compute the mean payoff, the total accumulated weight, and the discounted accumulated weight of the orbit under continuous weight functions and polynomial weight functions as a special case. Besides general LDSs, the special cases of stochastic LDSs and of LDSs with bounded orbits are considered. Furthermore, the problem of deciding whether an energy constraint is satisfied by the weighted orbit, i.e., whether the accumulated weight never drops below a given bound, is analysed.
|DOI Name=10.1145/3641513.3650173
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Datei:Logo-2 (1).jpg

2026-08-25T12:06:21Z

Rajab Aghamov:

Inproceedings2598778905

2026-08-25T11:58:34Z

Rajab Aghamov:

{{Publikation Erster Autor
|ErsterAutorVorname=Rajab
|ErsterAutorNachname=Aghamov
|FurtherAuthors=Christel Baier; Toghrul Karimov; Joël Ouaknine; Jakob Piribauer
}}
{{Inproceedings
|Referiert=0
|Title=Linear dynamical systems with continuous weight functions
|To appear=0
|Year=2024
|Booktitle=Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024, Hong Kong SAR, China, May 14-16, 2024
|Pages=22:1--22:11
|Publisher=ACM
|Editor=Erika Ábrahám and Manuel Mazo Jr.
}}
{{Publikation Details
|Bild=Logo-2.svg
|Abstract=In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight function assigning weights to the points in the orbit can be used to model quantitative aspects, such as resource consumption, of a system modelled by an LDS. This paper addresses the problems to compute the mean payoff, the total accumulated weight, and the discounted accumulated weight of the orbit under continuous weight functions and polynomial weight functions as a special case. Besides general LDSs, the special cases of stochastic LDSs and of LDSs with bounded orbits are considered. Furthermore, the problem of deciding whether an energy constraint is satisfied by the weighted orbit, i.e., whether the accumulated weight never drops below a given bound, is analysed.
|DOI Name=10.1145/3641513.3650173
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Datei:Logo-2.svg

2026-08-25T11:58:26Z

Rajab Aghamov:

Inproceedings3478

2026-08-25T11:56:34Z

Rajab Aghamov:

{{Publikation Erster Autor
|ErsterAutorVorname=Rajab
|ErsterAutorNachname=Aghamov
|FurtherAuthors=Christel Baier; Toghrul Karimov; Rupak Majumdar; Joël Ouaknine; Jakob Piribauer; Timm Spork
}}
{{Inproceedings
|Referiert=1
|Title=Model Checking Linear Temporal Logic with Standpoint Modalities
|To appear=0
|Year=2025
|Booktitle=Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning
|Pages=2--11
|Publisher=IJCAI Organization
|Editor=Magdalena Ortiz, Renata Wassermann, Torsten Schaub
}}
{{Publikation Details
|Bild=Cover.svg
|Abstract=Standpoint linear temporal logic (SLTL) is a recently introduced extension of classical linear temporal logic (LTL) with standpoint modalities. Intuitively, these modalities allow to express that, from agent a's standpoint, it is conceivable that a given formula holds. Besides the standard interpretation of the standpoint modalities we introduce four new semantics, which differ in the information an agent can extract from the history. We provide a general model checking algorithm applicable to SLTL under any of the five semantics. Furthermore we analyze the computational complexity of the corresponding model checking problems, obtaining PSPACE-completeness in three cases, which stands in contrast to the known EXPSPACE-completeness of the SLTL satisfiability problem.
|ISBN=2334-1033
|ISSN=978-1-956792-08-9
|Projekt=CPEC, SECAI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
|BibTex=@inproceedings{KR2025-1,
title = {{Model Checking Linear Temporal Logic with Standpoint Modalities}},
author = {Aghamov, Rajab and Baier, Christel and Karimov, Toghrul and Majumdar, Rupak and Ouaknine, Joël and Piribauer, Jakob and Spork, Timm},
booktitle = {{Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning}},
pages = {2--11},
year = {2025},
month = {10},
doi = {10.24963/kr.2025/1},
url = {https://doi.org/10.24963/kr.2025/1},
}
}}

Datei:Cover.svg

2026-08-25T11:56:31Z

Rajab Aghamov:

Article3125

2026-08-25T11:53:35Z

Rajab Aghamov:

{{Publikation Erster Autor
|ErsterAutorVorname=Rajab
|ErsterAutorNachname=Aghamov
|FurtherAuthors=Christel Baier; Toghrul Karimov; Joël Ouaknine; Jakob Piribauer
}}
{{Article
|Referiert=1
|Title=Linear dynamical systems with weight functions
|To appear=0
|Year=2026
|Journal=Nonlinear Analysis: Hybrid Systems
|Volume=60
|Pages=101680
|Publisher=Elsevier
}}
{{Publikation Details
|Bild=X1751570X.jpg
|Abstract=In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight function assigning weights to the points in the orbit can be used to model quantitative aspects, such as resource consumption, of a system modelled by an LDS. This paper addresses the problems of how to compute the mean payoff, the total accumulated weight, and the discounted accumulated weight of the orbit under continuous weight functions as well as polynomial weight functions as a special case. Additionally, weight functions that are definable in an o-minimal extension of the theory of the reals with exponentiation, which can be shown to be piecewise continuous, are considered. In particular, good ergodic properties of o-minimal weight functions, instrumental to the computation of the mean payoff, are established. Besides general LDSs, the special cases of stochastic LDSs and LDSs with bounded orbits are addressed. Finally, the problem of deciding whether an energy constraint is satisfied by the weighted orbit, i.e., whether the accumulated weight never drops below a given bound, is analysed.
|DOI Name=10.1016/j.nahs.2026.101680
|Projekt=CPEC, CeTI, SECAI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Inproceedings3480

2026-08-25T11:52:43Z

Rajab Aghamov:

{{Publikation Erster Autor
|ErsterAutorVorname=Rajab
|ErsterAutorNachname=Aghamov
|FurtherAuthors=Andrey Kudinov; Maik Nguyen; Jakob Piribauer
}}
{{Inproceedings
|Referiert=1
|Title=On Modal Logics of Full Products of Neighborhood Frames
|To appear=0
|Year=2026
|Booktitle=Advances in Modal Logic
|Publisher=College Publications
|Volume=16
|Note=To appear
}}
{{Publikation Details
|Abstract=On the product of two neighborhood frames, three natural neighborhood functions can be defined: the horizontal one assigning to a point $(x,y)$ the set of all supersets of sets $U\times\{y\}$, where $U$ is a neighborhood of $x$; the vertical analog; and the product neighborhood function assigning as neighborhoods all supersets of sets $U\times V$, for neighborhoods $U$ of $x$ and $V$ of $y$.
We define the tri-modal logics $\mathsf{T}\times_n^+ \mathsf{T}$ and $\mathsf{D}\times_n^+ \mathsf{D}$ of classes of full products equipped with all three neighborhood functions of neighborhood frames validating the logic $\mathsf{T}$ or $\mathsf{D}$; thereby extending known product results for $\mathsf{S4}$ and $\mathsf{D4}$ to weaker systems. Two interaction principles arise: $(\mathsf{sub})=\Box p \rightarrow \Box_1 p \land \Box_2 p$ and $(\mathsf{mix})=\Box p \rightarrow \Box_1\Box_2 p \land \Box_2\Box_1 p$, where $\Box$ for the product neighborhood function and $\Box_1,\Box_2$ the horizontal and vertical ones. Namely, we show that
$\mathsf{T}\times_n^+ \mathsf{T} = \mathsf{T}\otimes \mathsf{T}\otimes \mathsf{T} + (\mathsf{mix})$
and
$\mathsf{D}\times_n^+ \mathsf{D} = \mathsf{D}\otimes \mathsf{D}\otimes \mathsf{D} + (\mathsf{mix})$, where $\otimes$ denotes fusion. Notably, $(\mathsf{sub})$ and $(\mathsf{mix})$ are equivalent over $\mathsf{S4}\otimes\mathsf{S4}\otimes\mathsf{S4}$ and thus $\mathsf{S4}\otimes\mathsf{S4}\otimes\mathsf{S4}+(\mathsf{mix})$ axiomatizes the logic of full products of topological spaces.
|Projekt=CPEC, SECAI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Inproceedings3480

2026-08-25T11:52:06Z

Rajab Aghamov: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Rajab |ErsterAutorNachname=Aghamov |FurtherAuthors=Andrey Kudinov; Maik Nguyen; Jakob Piribauer }} {{Inproceedings |Referiert=1 |Title=On Modal Logics of Full Products of Neighborhood Frames |To appear=0 |Year=2026 |Booktitle=Advances in Modal Logic |Publisher=College Publications |Volume=16 |Note=To appear }} {{Publikation Details |Abstract=On the product of two neighborhood frames, three natural neighborhoo…“

{{Publikation Erster Autor
|ErsterAutorVorname=Rajab
|ErsterAutorNachname=Aghamov
|FurtherAuthors=Andrey Kudinov; Maik Nguyen; Jakob Piribauer
}}
{{Inproceedings
|Referiert=1
|Title=On Modal Logics of Full Products of Neighborhood Frames
|To appear=0
|Year=2026
|Booktitle=Advances in Modal Logic
|Publisher=College Publications
|Volume=16
|Note=To appear
}}
{{Publikation Details
|Abstract=On the product of two neighborhood frames, three natural neighborhood functions can be defined: the horizontal one assigning to a point $(x,y)$ the set of all supersets of sets $U\times\{y\}$, where $U$ is a neighborhood of $x$; the vertical analog; and the product neighborhood function assigning as neighborhoods all supersets of sets $U\times V$, for neighborhoods $U$ of $x$ and $V$ of $y$.
We define the tri-modal logics $\mathsf{T}\times_n^+ \mathsf{T}$ and $\mathsf{D}\times_n^+ \mathsf{D}$ of classes of full products equipped with all three neighborhood functions of neighborhood frames validating the logic $\mathsf{T}$ or $\mathsf{D}$; thereby extending known product results for $\mathsf{S4}$ and $\mathsf{D4}$ to weaker systems. Two interaction principles arise: $(\mathsf{sub})=\Box p \rightarrow \Box_1 p \land \Box_2 p$ and $(\mathsf{mix})=\Box p \rightarrow \Box_1\Box_2 p \land \Box_2\Box_1 p$, where $\Box$ for the product neighborhood function and $\Box_1,\Box_2$ the horizontal and vertical ones. Namely, we show that
$\mathsf{T}\times_n^+ \mathsf{T} = \mathsf{T}\otimes \mathsf{T}\otimes \mathsf{T} + (\mathsf{mix})$
and
$\mathsf{D}\times_n^+ \mathsf{D} = \mathsf{D}\otimes \mathsf{D}\otimes \mathsf{D} + (\mathsf{mix})$,
where $\otimes$ denotes fusion. Notably, $(\mathsf{sub})$ and $(\mathsf{mix})$ are equivalent over $\mathsf{S4}\otimes\mathsf{S4}\otimes\mathsf{S4}$ and thus $\mathsf{S4}\otimes\mathsf{S4}\otimes\mathsf{S4}+(\mathsf{mix})$ axiomatizes the logic of full products of topological spaces.
|Projekt=CPEC, SECAI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Article3125

2026-08-25T11:38:20Z

Rajab Aghamov:

{{Publikation Erster Autor
|ErsterAutorVorname=Rajab
|ErsterAutorNachname=Aghamov
|FurtherAuthors=Christel Baier; Toghrul Karimov; Joël Ouaknine; Jakob Piribauer
}}
{{Article
|Referiert=0
|Title=Linear dynamical systems with weight functions
|To appear=0
|Year=2026
|Journal=Nonlinear Analysis: Hybrid Systems
|Volume=60
|Pages=101680
|Publisher=Elsevier
}}
{{Publikation Details
|Bild=X1751570X.jpg
|Abstract=In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight function assigning weights to the points in the orbit can be used to model quantitative aspects, such as resource consumption, of a system modelled by an LDS. This paper addresses the problems of how to compute the mean payoff, the total accumulated weight, and the discounted accumulated weight of the orbit under continuous weight functions as well as polynomial weight functions as a special case. Additionally, weight functions that are definable in an o-minimal extension of the theory of the reals with exponentiation, which can be shown to be piecewise continuous, are considered. In particular, good ergodic properties of o-minimal weight functions, instrumental to the computation of the mean payoff, are established. Besides general LDSs, the special cases of stochastic LDSs and LDSs with bounded orbits are addressed. Finally, the problem of deciding whether an energy constraint is satisfied by the weighted orbit, i.e., whether the accumulated weight never drops below a given bound, is analysed.
|DOI Name=10.1016/j.nahs.2026.101680
|Projekt=CPEC, CeTI, SECAI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Article3125

2026-08-25T11:35:08Z

Rajab Aghamov: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Rajab |ErsterAutorNachname=Aghamov |FurtherAuthors=Christel Baier; Toghrul Karimov; Joël Ouaknine; Jakob Piribauer }} {{Article |Referiert=0 |Title=Linear dynamical systems, Formal verification, Linear recurrence sequences, Markov chains |To appear=0 |Year=2026 |Journal=Nonlinear Analysis: Hybrid Systems |Volume=60 |Pages=101680 |Publisher=Elsevier }} {{Publikation Details |Bild=X1751570X.jpg |Abstract=In di…“

{{Publikation Erster Autor
|ErsterAutorVorname=Rajab
|ErsterAutorNachname=Aghamov
|FurtherAuthors=Christel Baier; Toghrul Karimov; Joël Ouaknine; Jakob Piribauer
}}
{{Article
|Referiert=0
|Title=Linear dynamical systems, Formal verification, Linear recurrence sequences, Markov chains
|To appear=0
|Year=2026
|Journal=Nonlinear Analysis: Hybrid Systems
|Volume=60
|Pages=101680
|Publisher=Elsevier
}}
{{Publikation Details
|Bild=X1751570X.jpg
|Abstract=In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight function assigning weights to the points in the orbit can be used to model quantitative aspects, such as resource consumption, of a system modelled by an LDS. This paper addresses the problems of how to compute the mean payoff, the total accumulated weight, and the discounted accumulated weight of the orbit under continuous weight functions as well as polynomial weight functions as a special case. Additionally, weight functions that are definable in an o-minimal extension of the theory of the reals with exponentiation, which can be shown to be piecewise continuous, are considered. In particular, good ergodic properties of o-minimal weight functions, instrumental to the computation of the mean payoff, are established. Besides general LDSs, the special cases of stochastic LDSs and LDSs with bounded orbits are addressed. Finally, the problem of deciding whether an energy constraint is satisfied by the weighted orbit, i.e., whether the accumulated weight never drops below a given bound, is analysed.
|DOI Name=10.1016/j.nahs.2026.101680
|Projekt=CPEC, CeTI, SECAI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Datei:X1751570X.jpg

2026-08-25T11:29:26Z

Rajab Aghamov:

Inproceedings3479

2026-08-25T11:12:31Z

Rajab Aghamov: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Rajab |ErsterAutorNachname=Aghamov |FurtherAuthors=Christel Baier; Joël Ouaknine; Jakob Piribauer; Mihir Vahanwala; Isa Vialard }} {{Inproceedings |Referiert=1 |Title=Temporal Properties of Conditional Independence in Dynamic Bayesian Networks |To appear=0 |Year=2026 |Booktitle=Proceedings of the 40th Annual AAAI Conference on Artificial Intelligence (AAAI-26) |Pages=36601–36609 |Publisher=AAAI Press |Edit…“

{{Publikation Erster Autor
|ErsterAutorVorname=Rajab
|ErsterAutorNachname=Aghamov
|FurtherAuthors=Christel Baier; Joël Ouaknine; Jakob Piribauer; Mihir Vahanwala; Isa Vialard
}}
{{Inproceedings
|Referiert=1
|Title=Temporal Properties of Conditional Independence in Dynamic Bayesian Networks
|To appear=0
|Year=2026
|Booktitle=Proceedings of the 40th Annual AAAI Conference on Artificial Intelligence (AAAI-26)
|Pages=36601–36609
|Publisher=AAAI Press
|Editor=Sven Koenig, Chad Jenkins, Matthew E. Taylor
|Volume=40
}}
{{Publikation Details
|Bild=AAAI26Proceedings-Cover.jpg
|Abstract=Dynamic Bayesian networks (DBNs) are compact graphical representations used to model probabilistic systems where interdependent random variables and their distributions evolve over time. In this paper, we study the verification of the evolution of conditional-independence (CI) propositions against temporal logic specifications. To this end, we consider two specification formalisms over CI propositions: linear temporal logic (LTL), and non-deterministic Büchi automata (NBAs). This problem has two variants. Stochastic CI properties take the given concrete probability distributions into account, while structural CI properties are viewed purely in terms of the graphical structure of the DBN. We show that deciding whether a stochastic CI proposition eventually holds is at least as hard as the Skolem problem for linear recurrence sequences, which is a long-standing open problem in number theory. On the other hand, we show that verifying the evolution of structural CI propositions against LTL and NBA specifications is in PSPACE, and is hard for both NP and coNP. We also identify natural restrictions on the graphical structure of the DBN that make the verification of structural CI properties tractable.
|ISBN=10: 1-57735-906-2
|ISSN=13: 978-1-57735-906-7
|DOI Name=10.1609/aaai.v40i43.40983
|Projekt=CPEC, CeTI, SECAI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Datei:AAAI26Proceedings-Cover.jpg

2026-08-25T11:12:19Z

Rajab Aghamov:

Inproceedings3478

2026-08-25T07:57:41Z

Rajab Aghamov: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Rajab |ErsterAutorNachname=Aghamov |FurtherAuthors=Christel Baier; Toghrul Karimov; Rupak Majumdar; Joël Ouaknine; Jakob Piribauer; Timm Spork }} {{Inproceedings |Referiert=1 |Title=Model Checking Linear Temporal Logic with Standpoint Modalities |To appear=0 |Year=2025 |Booktitle=Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning |Pages=2--11 |Publisher=I…“

{{Publikation Erster Autor
|ErsterAutorVorname=Rajab
|ErsterAutorNachname=Aghamov
|FurtherAuthors=Christel Baier; Toghrul Karimov; Rupak Majumdar; Joël Ouaknine; Jakob Piribauer; Timm Spork
}}
{{Inproceedings
|Referiert=1
|Title=Model Checking Linear Temporal Logic with Standpoint Modalities
|To appear=0
|Year=2025
|Booktitle=Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning
|Pages=2--11
|Publisher=IJCAI Organization
|Editor=Magdalena Ortiz, Renata Wassermann, Torsten Schaub
}}
{{Publikation Details
|Abstract=Standpoint linear temporal logic (SLTL) is a recently introduced extension of classical linear temporal logic (LTL) with standpoint modalities. Intuitively, these modalities allow to express that, from agent a's standpoint, it is conceivable that a given formula holds. Besides the standard interpretation of the standpoint modalities we introduce four new semantics, which differ in the information an agent can extract from the history. We provide a general model checking algorithm applicable to SLTL under any of the five semantics. Furthermore we analyze the computational complexity of the corresponding model checking problems, obtaining PSPACE-completeness in three cases, which stands in contrast to the known EXPSPACE-completeness of the SLTL satisfiability problem.
|ISBN=2334-1033
|ISSN=978-1-956792-08-9
|Projekt=CPEC, SECAI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
|BibTex=@inproceedings{KR2025-1,
title = {{Model Checking Linear Temporal Logic with Standpoint Modalities}},
author = {Aghamov, Rajab and Baier, Christel and Karimov, Toghrul and Majumdar, Rupak and Ouaknine, Joël and Piribauer, Jakob and Spork, Timm},
booktitle = {{Proceedings of the 22nd International Conference on Principles of Knowledge Representation and Reasoning}},
pages = {2--11},
year = {2025},
month = {10},
doi = {10.24963/kr.2025/1},
url = {https://doi.org/10.24963/kr.2025/1},
}
}}

Rajab Aghamov

2023-02-12T22:06:17Z

Rajab Aghamov:

{{Mitarbeiter
|Vorname=Rajab
|Nachname=Aghamov
|Forschungsgruppe=Verifikation und formale quantitative Analyse; Wissensbasierte Systeme
|Stellung=Doktorand
|Ehemaliger=0
|Email=rajab.aghamov@tu-dresden.de
|Raum=3009
|Bild=Photo 2023-02-01 01-33-37.jpg
|Publikationen anzeigen=1
|Abschlussarbeiten anzeigen=0
}}

Rajab Aghamov

2023-02-09T10:32:13Z

Rajab Aghamov:

{{Mitarbeiter
|Vorname=Rajab
|Nachname=Aghamov
|Forschungsgruppe=Verifikation und formale quantitative Analyse; Wissensbasierte Systeme
|Stellung=Doktorand
|Ehemaliger=0
|Bild=Photo 2023-02-01 01-33-37.jpg
|Publikationen anzeigen=1
|Abschlussarbeiten anzeigen=0
}}

Datei:Photo 2023-02-01 01-33-37.jpg

2023-02-09T10:31:53Z

Rajab Aghamov: