136:
271:, recommended the book to researchers, lecturers, students and engineers, calling the book "impressive". Laroussinie found the textbook comprehensive and accessibly written, with a good number of examples, exercises and motivating ideas for key concepts. With a "unified framework", the first seven chapters cover classical theory and the last three chapters cover extensions of model checking.
280:, Gabriel Ciobanu believed the textbook could be used in advanced undergraduate or graduate courses, and would be useful to researchers. Ciobanu praised the "clear and intuitive" presentation and said it "should be appreciated for its pedagogical approach to covering basic concepts, deep theoretical results, and advanced topics in model checking research".
27:
194:
property, such as "a shared resource will always eventually be made available to a component that requests it", is of the form "a desirable outcome will eventually happen". Fairness properties such as "a traffic light never stops changing colour" can be used as
155:
might satisfy the property "the balance can never fall below €0,00". A video game might enforce the rule "if the player has 0 lives then the game ends in a loss". Both the vending machine and video game can be modelled as
244:
that aim to reduce the computation required to verify properties of a model. The ninth and tenth chapters are about extensions to the logics and automata previously considered, including through addition of a clock speed
356:
160:. Model checking is the process of describing such requirements in mathematical language, and automating proofs that the model satisfies the requirements, or discovery of
229:
player passes 'Go' infinitely often"; CTL encodes requirements about states in a system, such as "from any position, all players can eventually land on 'Go'".
399:
433:
94:
26:
428:
233:
formulae, which combine the two grammars, are also defined. Algorithms for model-checking formulae in these logics are given.
225:(CTL), two classes of formula that express properties. LTL encodes requirements about paths through a system, such as "every
168:
187:
354:
Kousha, Kayvan; Thelwall, Mike (1 March 2016). "Can Amazon.com
Reviews Help to Assess the Wider Impacts of Books?".
334:
241:
214:
that model the languages. It gives model-checking algorithms to verify properties or find counterexamples.
115:
that automates the problem of determining if a machine meets specification requirements. It was written by
250:
222:
207:
179:
339:
276:
218:
413:
151:: a model of a machine or process can be analysed to see if desirable properties hold. For instance, a
306:
267:
175:(set of instructions) can be carried out simultaneously by different machines or parts of a machine.
284:
120:
44:
393:
211:
157:
140:
89:
315:
203:
112:
386:
382:
226:
183:
152:
135:
246:
161:
148:
116:
108:
54:
40:
422:
254:
237:
196:
283:
In 2014, the book was one of the five most-cited academic texts monitored by the
190:
states are possible", is of the form "an undesirable outcome can never occur". A
236:
The seventh chapter explores formal ways to compare transition systems, such as
377:
319:
172:
124:
64:
191:
178:
Chapters 3 explores types of rules that a transition system may satisfy:
304:
Laroussinie, François (2010). "Principles of Model
Checking (Review)".
134:
357:
Journal of the
Association for Information Science and Technology
230:
167:
The second chapter focuses on creating an appropriate model for
199:
i.e. assumptions from which other properties can be deduced.
147:
The introduction and first chapter outline the field of
210:
language properties, and theoretical machines such as
88:
80:
70:
60:
50:
36:
8:
19:
25:
18:
335:"Principles of Model Checking (Review)"
296:
391:
217:The fifth and sixth chapters explore
7:
398:: CS1 maint: untitled periodical (
333:Ciobanu, Gabriel (8 January 2009).
14:
265:François Laroussinie, writing in
1:
171:, where multiple parts of an
20:Principles of Model Checking
202:The fourth chapter is about
104:Principles of Model Checking
123:, and published in 2008 by
450:
434:Computer science textbooks
24:
16:Computer science textbook
242:partial order reductions
164:if the model is faulty.
143:used to model a process
429:2008 non-fiction books
375:Lange, Martin (2010),
251:probabilistic automata
240:; the eighth is about
223:computation tree logic
180:linear time properties
144:
340:ACM Computing Reviews
320:10.1093/comjnl/bxp025
277:ACM Computing Reviews
219:linear temporal logic
138:
307:The Computer Journal
268:The Computer Journal
249:) or probabilities (
285:Book Citation Index
121:Joost-Pieter Katoen
45:Joost-Pieter Katoen
21:
169:concurrent systems
158:transition systems
145:
141:transition system
107:is a textbook on
100:
99:
441:
414:Official website
403:
397:
389:
362:
361:
351:
345:
344:
330:
324:
323:
301:
113:computer science
72:Publication date
29:
22:
449:
448:
444:
443:
442:
440:
439:
438:
419:
418:
410:
390:
374:
371:
369:Further reading
366:
365:
353:
352:
348:
332:
331:
327:
303:
302:
298:
293:
263:
184:safety property
162:counterexamples
153:vending machine
133:
73:
32:
17:
12:
11:
5:
447:
445:
437:
436:
431:
421:
420:
417:
416:
409:
408:External links
406:
405:
404:
370:
367:
364:
363:
346:
325:
314:(5): 615–616.
295:
294:
292:
289:
262:
259:
247:timed automata
212:Büchi automata
186:, such as "no
149:model checking
132:
129:
117:Christel Baier
109:model checking
98:
97:
92:
86:
85:
82:
78:
77:
74:
71:
68:
67:
62:
58:
57:
55:Model checking
52:
48:
47:
41:Christel Baier
38:
34:
33:
30:
15:
13:
10:
9:
6:
4:
3:
2:
446:
435:
432:
430:
427:
426:
424:
415:
412:
411:
407:
401:
395:
388:
384:
380:
379:
373:
372:
368:
359:
358:
350:
347:
342:
341:
336:
329:
326:
321:
317:
313:
309:
308:
300:
297:
290:
288:
286:
281:
279:
278:
272:
270:
269:
260:
258:
256:
255:Markov chains
252:
248:
243:
239:
234:
232:
228:
224:
220:
215:
213:
209:
205:
200:
198:
197:preconditions
193:
189:
185:
181:
176:
174:
170:
165:
163:
159:
154:
150:
142:
137:
130:
128:
126:
122:
118:
114:
111:, an area of
110:
106:
105:
96:
95:9780262026499
93:
91:
87:
83:
79:
76:25 April 2008
75:
69:
66:
63:
59:
56:
53:
49:
46:
42:
39:
35:
28:
23:
376:
355:
349:
338:
328:
311:
305:
299:
282:
275:
273:
266:
264:
238:bisimulation
235:
216:
201:
177:
166:
146:
103:
102:
101:
253:, based on
139:An example
31:Front cover
423:Categories
378:MathSciNet
291:References
221:(LTL) and
261:Reception
208:ω-regular
173:algorithm
125:MIT Press
65:MIT Press
61:Publisher
394:citation
287:(BKCI).
227:Monopoly
192:liveness
188:deadlock
131:Synopsis
387:2493187
204:regular
51:Subject
385:
360:: 580.
37:Author
81:Pages
400:link
231:CTL*
206:and
182:. A
119:and
90:ISBN
43:and
316:doi
274:In
257:).
84:975
425::
396:}}
392:{{
383:MR
381:,
337:.
312:53
310:.
127:.
402:)
343:.
322:.
318::
245:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
