Principles of Model Checking
ಮಾದರಿ ಪರಿಶೀಲನೆಯ ತತ್ವಗಳು ಮಾದರಿ ಪರಿಶೀಲನೆಯ ಪಠ್ಯಪುಸ್ತಕವಾಗಿದ್ದು, ಯಂತ್ರವು ನಿರ್ದಿಷ್ಟತೆಯ ಅವಶ್ಯಕತೆಗಳನ್ನು ಪೂರೈಸುತ್ತದೆಯೇ ಎಂದು ನಿರ್ಧರಿಸುವ ಸಮಸ್ಯೆಯನ್ನು ಸ್ವಯಂಚಾಲಿತಗೊಳಿಸುವ ಕಂಪ್ಯೂಟರ್ ವಿಜ್ಞಾನದ ಒಂದು ಕ್ಷೇತ್ರವಾಗಿದೆ. ಇದನ್ನು ಕ್ರಿಸ್ಟೆಲ್ ಬಾಯರ್ ಮತ್ತು ಜೂಸ್ಟ್-ಪೀಟರ್ ಕ್ಯಾಟೊಯೆನ್ ಬರೆದಿದ್ದಾರೆ ಮತ್ತು 2008 ರಲ್ಲಿ ಎಂಐಟಿ ಪ್ರೆಸ್ ಪ್ರಕಟಿಸಿದೆ. ಪರಿಚಯ ಮತ್ತು ಮೊದಲ ಅಧ್ಯಾಯವು ಮಾದರಿ ಪರಿಶೀಲನೆಯ ಕ್ಷೇತ್ರವನ್ನು ರೂಪಿಸುತ್ತದೆಃ ಯಂತ್ರ ಅಥವಾ ಪ್ರಕ್ರಿಯೆಯ ಮಾದರಿಯು ಅಪೇಕ್ಷಣೀಯ ಗುಣಲಕ್ಷಣಗಳನ್ನು ಹೊಂದಿದೆಯೇ ಎಂದು ನೋಡಲು ವಿಶ್ಲೇಷಿಸಬಹುದು. ಉದಾಹರಣೆಗೆ, ಮಾರಾಟ ಯಂತ್ರವು "ಬಾಕಿಯು ಎಂದಿಗೂ 0,00 ಯುರೋಗಳಿಗಿಂತ ಕಡಿಮೆಯಾಗುವುದಿಲ್ಲ" ಎಂಬ ಆಸ್ತಿಯನ್ನು ತೃಪ್ತಿಪಡಿಸಬಹುದು. ವೀಡಿಯೊ ಆಟವು "ಆಟಗಾರನು 0 ಜೀವಗಳನ್ನು ಹೊಂದಿದ್ದರೆ ಆಟವು ನಷ್ಟದಲ್ಲಿ ಕೊನೆಗೊಳ್ಳುತ್ತದೆ" ಎಂಬ ನಿಯಮವನ್ನು ಜಾರಿಗೊಳಿಸಬಹುದು. ಮಾರಾಟ ಯಂತ್ರ ಮತ್ತು ವಿಡಿಯೋ ಗೇಮ್ ಎರಡನ್ನೂ ಪರಿವರ್ತನಾ ವ್ಯವಸ್ಥೆಗಳಾಗಿ ರೂಪಿಸಬಹುದು. ಮಾದರಿ ಪರಿಶೀಲನೆ ಎಂದರೆ ಅಂತಹ ಅವಶ್ಯಕತೆಗಳನ್ನು ಗಣಿತದ ಭಾಷೆಯಲ್ಲಿ ವಿವರಿಸುವ ಪ್ರಕ್ರಿಯೆ, ಮತ್ತು ಮಾದರಿಯು ಅವಶ್ಯಕತೆಗಳನ್ನು ಪೂರೈಸುತ್ತದೆ ಎಂಬುದಕ್ಕೆ ಪುರಾವೆಗಳನ್ನು ಸ್ವಯಂಚಾಲಿತಗೊಳಿಸುವುದು, ಅಥವಾ ಮಾದರಿಯು ದೋಷಪೂರಿತವಾಗಿದ್ದರೆ ಪ್ರತಿ ನಿದರ್ಶನಗಳನ್ನು ಕಂಡುಹಿಡಿಯುವುದು. ಎರಡನೇ ಅಧ್ಯಾಯವು ಸಮವರ್ತಿ ವ್ಯವಸ್ಥೆಗಳಿಗೆ ಸೂಕ್ತವಾದ ಮಾದರಿಯನ್ನು ರಚಿಸುವುದರ ಮೇಲೆ ಕೇಂದ್ರೀಕರಿಸುತ್ತದೆ, ಅಲ್ಲಿ ಅಲ್ಗಾರಿದಮ್ನ ಅನೇಕ ಭಾಗಗಳನ್ನು (ಸೂಚನೆಗಳ ಸೆಟ್) ವಿವಿಧ ಯಂತ್ರಗಳು ಅಥವಾ ಯಂತ್ರದ ಭಾಗಗಳಿಂದ ಏಕಕಾಲದಲ್ಲಿ ನಿರ್ವಹಿಸಬಹುದು. 3ನೇ ಅಧ್ಯಾಯವು ಪರಿವರ್ತನೆಯ ವ್ಯವಸ್ಥೆಯು ಪೂರೈಸಬಹುದಾದ ನಿಯಮಗಳ ಪ್ರಕಾರಗಳನ್ನು ಅನ್ವೇಷಿಸುತ್ತದೆಃ ರೇಖೀಯ ಸಮಯದ ಗುಣಲಕ್ಷಣಗಳು. "ಯಾವುದೇ ಡೆಡ್ಲಾಕ್ ಸ್ಥಿತಿಗಳು ಸಾಧ್ಯವಿಲ್ಲ" ಎಂಬಂತಹ ಸುರಕ್ಷತಾ ಗುಣಲಕ್ಷಣವು "ಅನಪೇಕ್ಷಿತ ಫಲಿತಾಂಶವು ಎಂದಿಗೂ ಸಂಭವಿಸುವುದಿಲ್ಲ" ಎಂಬ ರೂಪದಲ್ಲಿದೆ. "ಹಂಚಿಕೊಂಡ ಸಂಪನ್ಮೂಲವನ್ನು ವಿನಂತಿಸುವ ಘಟಕಕ್ಕೆ ಅಂತಿಮವಾಗಿ ಯಾವಾಗಲೂ ಲಭ್ಯವಾಗುವಂತೆ ಮಾಡಲಾಗುತ್ತದೆ" ಎಂಬಂತಹ ಜೀವಂತ ಆಸ್ತಿಯು "ಅಂತಿಮವಾಗಿ ಅಪೇಕ್ಷಣೀಯ ಫಲಿತಾಂಶವು ಸಂಭವಿಸುತ್ತದೆ" ಎಂಬ ರೂಪದಲ್ಲಿದೆ. "ಟ್ರಾಫಿಕ್ ಲೈಟ್ ಎಂದಿಗೂ ಬಣ್ಣವನ್ನು ಬದಲಾಯಿಸುವುದನ್ನು ನಿಲ್ಲಿಸುವುದಿಲ್ಲ" ಎಂಬಂತಹ ನ್ಯಾಯೋಚಿತ ಗುಣಲಕ್ಷಣಗಳನ್ನು ಪೂರ್ವ ಷರತ್ತುಗಳಾಗಿ ಬಳಸಬಹುದು. ಇತರ ಗುಣಲಕ್ಷಣಗಳನ್ನು ಯಾವ ಊಹೆಗಳಿಂದ ಊಹಿಸಬಹುದು. ನಾಲ್ಕನೇ ಅಧ್ಯಾಯವು ನಿಯಮಿತ ಮತ್ತು ω-ನಿಯಮಿತ ಭಾಷಾ ಗುಣಲಕ್ಷಣಗಳ ಬಗ್ಗೆ ಮತ್ತು ಭಾಷೆಗಳನ್ನು ರೂಪಿಸುವ ಬುಚಿ ಆಟೋಮಾಟಾದಂತಹ ಸೈದ್ಧಾಂತಿಕ ಯಂತ್ರಗಳ ಬಗ್ಗೆ ಇದೆ. ಇದು ಗುಣಲಕ್ಷಣಗಳನ್ನು ಪರಿಶೀಲಿಸಲು ಅಥವಾ ಪ್ರತಿರೂಪಗಳನ್ನು ಕಂಡುಹಿಡಿಯಲು ಮಾದರಿ-ಪರಿಶೀಲನಾ ಕ್ರಮಾವಳಿಗಳನ್ನು ನೀಡುತ್ತದೆ. ಐದನೇ ಮತ್ತು ಆರನೇ ಅಧ್ಯಾಯಗಳು ಗುಣಲಕ್ಷಣಗಳನ್ನು ವ್ಯಕ್ತಪಡಿಸುವ ಎರಡು ವರ್ಗದ ಸೂತ್ರಗಳಾದ ಲೀನಿಯರ್ ಟೆಂಪೋರಲ್ ಲಾಜಿಕ್ (ಎಲ್. ಟಿ. ಎಲ್) ಮತ್ತು ಕಂಪ್ಯೂಟೇಶನ್ ಟ್ರೀ ಲಾಜಿಕ್ (ಸಿ. ಟಿ. ಎಲ್) ಅನ್ನು ಅನ್ವೇಷಿಸುತ್ತವೆ. ಎಲ್. ಟಿ. ಎಲ್. ಒಂದು ವ್ಯವಸ್ಥೆಯ ಮೂಲಕ ಹಾದುಹೋಗುವ ಮಾರ್ಗಗಳ ಬಗ್ಗೆ ಅವಶ್ಯಕತೆಗಳನ್ನು ಎನ್ಕೋಡ್ ಮಾಡುತ್ತದೆ, ಉದಾಹರಣೆಗೆ "ಪ್ರತಿಯೊಬ್ಬ ಏಕಸ್ವಾಮ್ಯ ಆಟಗಾರನು ಅನಂತವಾಗಿ 'ಗೋ' ಅನ್ನು ಹಾದುಹೋಗುತ್ತಾನೆ"; ಸಿ. ಟಿ. ಎಲ್. ಒಂದು ವ್ಯವಸ್ಥೆಯಲ್ಲಿನ ಸ್ಥಿತಿಗಳ ಬಗ್ಗೆ ಅವಶ್ಯಕತೆಗಳನ್ನು ಎನ್ಕೋಡ್ ಮಾಡುತ್ತದೆ, ಉದಾಹರಣೆಗೆ "ಯಾವುದೇ ಸ್ಥಾನದಿಂದ, ಎಲ್ಲಾ ಆಟಗಾರರು ಅಂತಿಮವಾಗಿ 'ಗೋ' ನಲ್ಲಿ ಇಳಿಯಬಹುದು". ಎರಡು ವ್ಯಾಕರಣಗಳನ್ನು ಸಂಯೋಜಿಸುವ ಸಿಟಿಎಲ್ * ಸೂತ್ರಗಳನ್ನು ಸಹ ವ್ಯಾಖ್ಯಾನಿಸಲಾಗಿದೆ. ಈ ತರ್ಕಗಳಲ್ಲಿ ಮಾದರಿ-ಪರಿಶೀಲನಾ ಸೂತ್ರಗಳಿಗೆ ಕ್ರಮಾವಳಿಗಳನ್ನು ನೀಡಲಾಗಿದೆ. ಏಳನೇ ಅಧ್ಯಾಯವು ದ್ವಿಗುಣಗೊಳಿಸುವಿಕೆಯಂತಹ ಪರಿವರ್ತನಾ ವ್ಯವಸ್ಥೆಗಳನ್ನು ಹೋಲಿಸುವ ಔಪಚಾರಿಕ ಮಾರ್ಗಗಳನ್ನು ಅನ್ವೇಷಿಸುತ್ತದೆ; ಎಂಟನೇ ಅಧ್ಯಾಯವು ಮಾದರಿಯ ಗುಣಲಕ್ಷಣಗಳನ್ನು ಪರಿಶೀಲಿಸಲು ಅಗತ್ಯವಾದ ಗಣನೆಯನ್ನು ಕಡಿಮೆ ಮಾಡುವ ಗುರಿಯನ್ನು ಹೊಂದಿರುವ ಭಾಗಶಃ ಕ್ರಮ ಕಡಿತಗಳ ಬಗ್ಗೆ ಇದೆ. ಒಂಬತ್ತನೇ ಮತ್ತು ಹತ್ತನೇ ಅಧ್ಯಾಯಗಳು ಗಡಿಯಾರದ ವೇಗ (ಸಮಯದ ಸ್ವಯಂಚಾಲಿತ) ಅಥವಾ ಸಂಭವನೀಯತೆಗಳನ್ನು (ಮಾರ್ಕೋವ್ ಸರಪಳಿಗಳ ಆಧಾರದ ಮೇಲೆ ಸಂಭವನೀಯ ಸ್ವಯಂಚಾಲಿತ) ಸೇರಿಸುವ ಮೂಲಕ ಈ ಹಿಂದೆ ಪರಿಗಣಿಸಲಾದ ತರ್ಕ ಮತ್ತು ಸ್ವಯಂಚಾಲಿತತೆಯ ವಿಸ್ತರಣೆಗಳ ಬಗ್ಗೆ ಇವೆ. ರಿಸೆಪ್ಷನ್ ಫ್ರಾಂಕೋಯಿಸ್ ಲಾರೌಸಿನಿ, ದಿ ಕಂಪ್ಯೂಟರ್ ಜರ್ನಲ್ನಲ್ಲಿ ಬರೆಯುತ್ತಾ, ಸಂಶೋಧಕರು, ಉಪನ್ಯಾಸಕರು, ವಿದ್ಯಾರ್ಥಿಗಳು ಮತ್ತು ಎಂಜಿನಿಯರ್ಗಳಿಗೆ ಪುಸ್ತಕವನ್ನು ಶಿಫಾರಸು ಮಾಡಿದರು, ಪುಸ್ತಕವನ್ನು "ಪ್ರಭಾವಶಾಲಿ" ಎಂದು ಕರೆದರು. ಉತ್ತಮ ಸಂಖ್ಯೆಯ ಉದಾಹರಣೆಗಳು, ಅಭ್ಯಾಸಗಳು ಮತ್ತು ಪ್ರಮುಖ ಪರಿಕಲ್ಪನೆಗಳಿಗೆ ಪ್ರೇರೇಪಿಸುವ ವಿಚಾರಗಳೊಂದಿಗೆ ಪಠ್ಯಪುಸ್ತಕವನ್ನು ಸಮಗ್ರವಾಗಿ ಮತ್ತು ಸುಲಭವಾಗಿ ಬರೆಯಲಾಗಿದೆ ಎಂದು ಲಾರೌಸಿನಿ ಕಂಡುಕೊಂಡರು. "ಏಕೀಕೃತ ಚೌಕಟ್ಟಿನೊಂದಿಗೆ", ಮೊದಲ ಏಳು ಅಧ್ಯಾಯಗಳು ಶಾಸ್ತ್ರೀಯ ಸಿದ್ಧಾಂತವನ್ನು ಒಳಗೊಂಡಿವೆ ಮತ್ತು ಕೊನೆಯ ಮೂರು ಅಧ್ಯಾಯಗಳು ಮಾದರಿ ಪರಿಶೀಲನೆಯ ವಿಸ್ತರಣೆಗಳನ್ನು ಒಳಗೊಂಡಿವೆ. ಎಸಿಎಂ ಕಂಪ್ಯೂಟಿಂಗ್ ರಿವ್ಯೂಸ್ನಲ್ಲಿ, ಗ್ಯಾಬ್ರಿಯಲ್ ಸಿಯೋಬಾನು ಈ ಪಠ್ಯಪುಸ್ತಕವನ್ನು ಮುಂದುವರಿದ ಪದವಿಪೂರ್ವ ಅಥವಾ ಪದವಿ ಕೋರ್ಸ್ಗಳಲ್ಲಿ ಬಳಸಬಹುದೆಂದು ನಂಬಿದ್ದರು ಮತ್ತು ಇದು ಸಂಶೋಧಕರಿಗೆ ಉಪಯುಕ್ತವಾಗಿದೆ. ಸಿಯೋಬಾನು "ಸ್ಪಷ್ಟ ಮತ್ತು ಅಂತರ್ಬೋಧೆಯ" ಪ್ರಸ್ತುತಿಯನ್ನು ಶ್ಲಾಘಿಸಿದರು ಮತ್ತು "ಮಾದರಿ ಪರಿಶೀಲನಾ ಸಂಶೋಧನೆಯಲ್ಲಿ ಮೂಲಭೂತ ಪರಿಕಲ್ಪನೆಗಳು, ಆಳವಾದ ಸೈದ್ಧಾಂತಿಕ ಫಲಿತಾಂಶಗಳು ಮತ್ತು ಸುಧಾರಿತ ವಿಷಯಗಳನ್ನು ಒಳಗೊಂಡಿರುವ ಅದರ ಶೈಕ್ಷಣಿಕ ವಿಧಾನಕ್ಕಾಗಿ ಇದನ್ನು ಪ್ರಶಂಸಿಸಬೇಕು" ಎಂದು ಹೇಳಿದರು. 2014ರಲ್ಲಿ, ಈ ಪುಸ್ತಕವು ಬುಕ್ ಸೈಟೇಶನ್ ಇಂಡೆಕ್ಸ್ (ಬಿ. ಕೆ. ಸಿ. ಐ) ಮೇಲ್ವಿಚಾರಣೆ ಮಾಡಿದ ಐದು ಹೆಚ್ಚು ಉಲ್ಲೇಖಿಸಲಾದ ಶೈಕ್ಷಣಿಕ ಪಠ್ಯಗಳಲ್ಲಿ ಒಂದಾಗಿತ್ತು. ಹೆಚ್ಚಿನ ಓದುವ ಉಲ್ಲೇಖಗಳು ಬಾಹ್ಯ ಕೊಂಡಿಗಳು ಅಧಿಕೃತ ಜಾಲತಾಣ 2008 ಕಾಲ್ಪನಿಕವಲ್ಲದ ಪುಸ್ತಕಗಳು ಕಂಪ್ಯೂಟರ್ ವಿಜ್ಞಾನ ಪಠ್ಯಪುಸ್ತಕಗಳು