<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=undefined&type=result"></script>');
-->
</script>

COPY SCRIPT

For further information contact us at helpdesk@openaire.eu

Computing Stuttering Simulations

descriptionPublicationkeyboard_double_arrow_right Part of book or chapter of book , Article , Preprint , Conference object 01 Jan 2009Embargo end date: 01 Jan 2009 Italy Publisher:Springer Berlin Heidelberg

Authors: RANZATO, FRANCESCO; TAPPARO, FRANCESCO;

doi: 10.1007/978-3-642-04081-8_36 , 10.48550/arxiv.0904.1488

arXiv: http://arxiv.org/abs/0904.1488

handle: 11577/2373872

Computing Stuttering Simulations

- Summary
- Subjects
- Related research
  (4)
- Metrics

Abstract

Stuttering bisimulation is a well-known behavioral equivalence that preserves CTL-X, namely CTL without the next-time operator X. Correspondingly, the stuttering simulation preorder induces a coarser behavioral equivalence that preserves the existential fragment ECTL-{X,G}, namely ECTL without the next-time X and globally G operators. While stuttering bisimulation equivalence can be computed by the well-known Groote and Vaandrager's [1990] algorithm, to the best of our knowledge, no algorithm for computing the stuttering simulation preorder and equivalence is available. This paper presents such an algorithm for finite state systems.

Country

Italy

Related Organizations

University of Padua
Italy

Keywords

FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Logic in Computer Science (cs.LO)

4 Research products, page 1 of 1

Abstractions and Partial Order Reductions for Checking Branching Properties of Time Petri Nets
2001IsAmongTopNSimilarDocuments
Slicing Petri Nets with an Application to Workflow Verification
2008IsAmongTopNSimilarDocuments
An expectation-transformer model for probabilistic temporal logic
1999IsAmongTopNSimilarDocuments
An Equivalence Based Method for Compositional Verification of the Linear Temporal Logic of Constraint Automata
2006IsAmongTopNSimilarDocuments

Impact byBIP!

	citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	6
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average