2 Search Results for "Hvid Hansen, Helle"


Document
Bisimulation for Weakly Expressive Coalgebraic Modal Logics

Authors: Zeinab Bakhtiari and Helle Hvid Hansen

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)


Abstract
Research on the expressiveness of coalgebraic modal logics with respect to semantic equivalence notions has so far focused mainly on finding logics that are able to distinguish states that are not behaviourally equivalent (such logics are said to be expressive). In other words, the notion of behavioural equivalence is taken as the starting point, and the expressiveness of the logic is evaluated against it. However, for some applications, modal logics that are not expressive are of independent interest. Such an example is given by contingency logic. We can now turn the question of expressiveness around and ask, given a modal logic, what is a suitable notion of semantic equivalence? In this paper, we propose a notion of \Lambda-bisimulation which is parametric in a collection \Lambda of predicate liftings. We study the basic properties of \Lambda-bisimilarity, and prove as our main result a Hennessy-Milner style theorem, which shows that (for finitary functors) \Lambda-bisimilarity exactly matches the expressiveness of the coalgebraic modal logic arising from \Lambda.

Cite as

Zeinab Bakhtiari and Helle Hvid Hansen. Bisimulation for Weakly Expressive Coalgebraic Modal Logics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{bakhtiari_et_al:LIPIcs.CALCO.2017.4,
  author =	{Bakhtiari, Zeinab and Hvid Hansen, Helle},
  title =	{{Bisimulation for Weakly Expressive Coalgebraic Modal Logics}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{4:1--4:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.4},
  URN =		{urn:nbn:de:0030-drops-80500},
  doi =		{10.4230/LIPIcs.CALCO.2017.4},
  annote =	{Keywords: Coalgebraic modal logic, bisimulation, expressiveness, Hennessy-Milner theorem}
}
Document
A Coinductive Framework for Infinitary Rewriting and Equational Reasoning

Authors: Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)


Abstract
We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.

Cite as

Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva. A Coinductive Framework for Infinitary Rewriting and Equational Reasoning. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 143-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{endrullis_et_al:LIPIcs.RTA.2015.143,
  author =	{Endrullis, J\"{o}rg and Hansen, Helle Hvid and Hendriks, Dimitri and Polonsky, Andrew and Silva, Alexandra},
  title =	{{A Coinductive Framework for Infinitary Rewriting and Equational Reasoning}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{143--159},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.143},
  URN =		{urn:nbn:de:0030-drops-51949},
  doi =		{10.4230/LIPIcs.RTA.2015.143},
  annote =	{Keywords: infinitary rewriting, coinduction}
}
  • Refine by Author
  • 1 Bakhtiari, Zeinab
  • 1 Endrullis, Jörg
  • 1 Hansen, Helle Hvid
  • 1 Hendriks, Dimitri
  • 1 Hvid Hansen, Helle
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 1 Coalgebraic modal logic
  • 1 Hennessy-Milner theorem
  • 1 bisimulation
  • 1 coinduction
  • 1 expressiveness
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2015
  • 1 2017

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail