Difference between revisions of "Publications/poitrenaud.19.icfem"

From LRDE

(Created page with "{{Publication | published = true | date = 2019-08-02 | authors = Denis Poitrenaud, Etienne Renault | title = Combining Parallel Emptiness Checks with Partial Order Reductions...")
 
 
Line 5: Line 5:
 
| title = Combining Parallel Emptiness Checks with Partial Order Reductions
 
| title = Combining Parallel Emptiness Checks with Partial Order Reductions
 
| booktitle = Proceedings of the 21st International Conference on Formal Engineering Methods (ICFEM'19)
 
| booktitle = Proceedings of the 21st International Conference on Formal Engineering Methods (ICFEM'19)
| editors = ??
+
| editors = Yamine Ait Ameur, Shengchao Qin
 
| address = Shenzhen, China
 
| address = Shenzhen, China
 
| pages = ?? to ??
 
| pages = ?? to ??
 
| publisher = Springer
 
| publisher = Springer
 
| series = Lecture Notes in Computer Science
 
| series = Lecture Notes in Computer Science
| volume = ??
+
| volume = 11852
 
| abstract = In explicit state model checking ofconcurrent systemsmulticore emptiness checks and partial order reductions (POR) are two major techniques to handle large state spaces. The first one tries to take advantage of multi-core architectures while the second one may decrease exponentially the size of the state space to explore. For checking LTL properties, Bloemen and van de Pol [2] shown that the best performance is currently obtained using their multi-core SCC-based emptiness check. However, combining the latest SCC-based algorithm with POR is not trivial since a condition on cycles, the proviso, must be enforced on an algorithm which processes collaboratively cycles. In this paper, we suggest a pessimistic approach to tackle this problem for liveness properties. For safety ones, we propose an algorithm which takes benefit from the information computed by the SCC-based algorithm. We also present new parallel provisos for both safety and liveness prop- erties that relies on other multi-core emptiness checks. We observe that all presented algorithms maintain good reductions and scalability.
 
| abstract = In explicit state model checking ofconcurrent systemsmulticore emptiness checks and partial order reductions (POR) are two major techniques to handle large state spaces. The first one tries to take advantage of multi-core architectures while the second one may decrease exponentially the size of the state space to explore. For checking LTL properties, Bloemen and van de Pol [2] shown that the best performance is currently obtained using their multi-core SCC-based emptiness check. However, combining the latest SCC-based algorithm with POR is not trivial since a condition on cycles, the proviso, must be enforced on an algorithm which processes collaboratively cycles. In this paper, we suggest a pessimistic approach to tackle this problem for liveness properties. For safety ones, we propose an algorithm which takes benefit from the information computed by the SCC-based algorithm. We also present new parallel provisos for both safety and liveness prop- erties that relies on other multi-core emptiness checks. We observe that all presented algorithms maintain good reductions and scalability.
 
| lrdeprojects = Spot
 
| lrdeprojects = Spot
Line 24: Line 24:
 
   booktitle = <nowiki>{</nowiki>Proceedings of the 21st International Conference on Formal
 
   booktitle = <nowiki>{</nowiki>Proceedings of the 21st International Conference on Formal
 
  Engineering Methods (ICFEM'19)<nowiki>}</nowiki>,
 
  Engineering Methods (ICFEM'19)<nowiki>}</nowiki>,
   editor = <nowiki>{</nowiki>??<nowiki>}</nowiki>,
+
   editor = <nowiki>{</nowiki>Yamine Ait Ameur and Shengchao Qin<nowiki>}</nowiki>,
 
   address = <nowiki>{</nowiki>Shenzhen, China<nowiki>}</nowiki>,
 
   address = <nowiki>{</nowiki>Shenzhen, China<nowiki>}</nowiki>,
 
   year = 2019,
 
   year = 2019,
Line 31: Line 31:
 
   publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
 
   publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>,
 
   series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
 
   series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>,
   volume = <nowiki>{</nowiki>??<nowiki>}</nowiki>,
+
   volume = <nowiki>{</nowiki>11852<nowiki>}</nowiki>,
 
   abstract = <nowiki>{</nowiki> In explicit state model checking ofconcurrent systems,
 
   abstract = <nowiki>{</nowiki> In explicit state model checking ofconcurrent systems,
 
  multicore emptiness checks and partial order reductions
 
  multicore emptiness checks and partial order reductions

Latest revision as of 09:47, 19 September 2019

Abstract

In explicit state model checking ofconcurrent systemsmulticore emptiness checks and partial order reductions (POR) are two major techniques to handle large state spaces. The first one tries to take advantage of multi-core architectures while the second one may decrease exponentially the size of the state space to explore. For checking LTL properties, Bloemen and van de Pol [2] shown that the best performance is currently obtained using their multi-core SCC-based emptiness check. However, combining the latest SCC-based algorithm with POR is not trivial since a condition on cycles, the proviso, must be enforced on an algorithm which processes collaboratively cycles. In this paper, we suggest a pessimistic approach to tackle this problem for liveness properties. For safety ones, we propose an algorithm which takes benefit from the information computed by the SCC-based algorithm. We also present new parallel provisos for both safety and liveness prop- erties that relies on other multi-core emptiness checks. We observe that all presented algorithms maintain good reductions and scalability.

Documents

Bibtex (lrde.bib)

@InProceedings{	  poitrenaud.19.icfem,
  author	= {Denis Poitrenaud and Etienne Renault},
  title		= {Combining Parallel Emptiness Checks with Partial Order
		  Reductions},
  booktitle	= {Proceedings of the 21st International Conference on Formal
		  Engineering Methods (ICFEM'19)},
  editor	= {Yamine Ait Ameur and Shengchao Qin},
  address	= {Shenzhen, China},
  year		= 2019,
  month		= nov,
  pages		= {??--??},
  publisher	= {Springer},
  series	= {Lecture Notes in Computer Science},
  volume	= {11852},
  abstract	= { In explicit state model checking ofconcurrent systems,
		  multicore emptiness checks and partial order reductions
		  (POR) are two major techniques to handle large state
		  spaces. The first one tries to take advantage of multi-core
		  architectures while the second one may decrease
		  exponentially the size of the state space to explore. For
		  checking LTL properties, Bloemen and van de Pol [2] shown
		  that the best performance is currently obtained using their
		  multi-core SCC-based emptiness check. However, combining
		  the latest SCC-based algorithm with POR is not trivial
		  since a condition on cycles, the proviso, must be enforced
		  on an algorithm which processes collaboratively cycles. In
		  this paper, we suggest a pessimistic approach to tackle
		  this problem for liveness properties. For safety ones, we
		  propose an algorithm which takes benefit from the
		  information computed by the SCC-based algorithm. We also
		  present new parallel provisos for both safety and liveness
		  prop- erties that relies on other multi-core emptiness
		  checks. We observe that all presented algorithms maintain
		  good reductions and scalability.}
}